As a side effect, this puts symbolic links back inside the archive. They
had been lost since 0.82 and prevented the use of a local installation.

Induction_pr performs induction on the leftmost application
of some inductive predicate in the goal.

This can be overriden by attaching the label "induction"
on such an application. In this case, any unlabeled application
will be ignored.

Inversion_pr works similarly, excepted that it does not generate
inductive hypotheses, but simply inverses inductive predicate.
In this case, the label "inversion" will be used.

Jacques-Pascal's idea, pushed a bit further

- add "-L theories" to options of why3realize for PVS
- look for the full installation path in the output of "isabelle
  components"

When "configure.in" has not changed, autoconf reads the content of
"autom4te", which contains the old version number.

and merge the why3 and why3session libraries back into one.