GitLab

  definitions in smtlib-bv driver.
- Add no-bv.gen driver file targeted to provers without support for
  the smtlib bv theory (or for the no_bv variants).
- update realization & tests

Isabelle2015 is still supported, but support for Isabelle2014 has been
discontinued.

for pi by the best possible bounds in double-precision IEEE-754
floating-point numbers

  + size -> size_bv
  + size_int -> size
  + change two_power_size and max_int definitions
  + add axioms to BVConverter
  + new axiom relating nth and nth_bv
  + some reorganisation
- update coq realisation
- modify in consequence the relevant examples and pull the completed ones out of in_progress

Realization of theory of reals needs to be included in the main realization
file, so it is visible by default when proving VCs in Isabelle.

Works both with Isabelle 2014 and 2015

Fix Bool.v
Add TODO to Seq.v and BV_Gen.v
update queens_bv session

Add int.NumOf realization.

Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

- generation in the makefile
- proofs done
Remove complex axioms from Pow2int in bv.why.
Add guards in rotates axioms in bv.why.