Give a git-like invocation to why3 tools.
update drivers and example mp after last Why3 GT
Add a "prove" subcommand.
Factor option parsing for why3 commands.
Make --realize into a proper subcommand.
Simplify code for why3realize.
Improve why3realize --help.
Partly adapt the bench to the new commands.
Add an extract command to why3.
Display available commands by default.
Add a why3execute command.
Fix bench.
Update documentation.
Eliminate if and let in formulae
Prefix names of lemmas / axioms with qualifier "facts"

This avoids clashes with definitions that happen to have the same name
Blacklist identifiers "o" and "O"

These identifiers are used as infix operators for the composition
of functions and relations in Isabelle/HOL
Split conjunctions in premises of rules
Added missing proofs
upgrade the Coq version in the examples
linear probing: work in progress