GitLab

# Conflicts:
#	examples/logic/einstein/why3session.xml
#	examples/prover/Unification/why3session.xml

This reverts commit 070328e5.
The theory for bv has not yet been changed in next so this makes
things fail to add this commit.

Conflicts:
	examples/regtests.sh

additional cosmetic changes

- do not erase Isabelle's XML files even in local mode

- use realization*s* with an s everywhere

generated again.

* Makefile.in
Realizations for isabelle are generated even if Isabelle is not installed.
The .thy file are checked only if isabelle is installed. This allows us
to treat it as with coq and be able to detect changes in realizations
with a script.
Dont erase xml generated file during clean.

* configure.in
Changed the configure to always generate a default isabelle version (set
to 2017) for generation of the realization driver (needed even when no
isablle support is given).

* examples/regtests.sh
Adding option --check-realization and --only-realization which add a test
the compares the output of the new realization compared to the one
recorded. It complains if they are different forcing the user to update the
realization files.

* lib/isabelle/*
Adding xml files corresponding to generated realization for Isabelle. This
allows for the abovementionned script to work even if Isabelle is not
installed (which is the case for most people editing theories).

* examples/nightly-bench.sh
Add the option for realization check

* misc/ci-bench
Calls the test for realization

Conflicts:
	examples/regtests.sh

* Makefile.in
Reordered Lib_transform into makefile.

* src/transform/ind_itp.ml
Adding a dependant revert transformation

* src/transform/ind_itp.mli
Adding a transformation that does a dependant revert of a list of symbols.

* src/transform/induction.ml
Adding transformation induction_ty_lex and induction_on_hyp.

* src/transform/induction_pr.ml
induction_arg_pr and inversion_arg_pr added.

formerly, replay could report success without signaling presence
of detached goals.

Should not happen anymore

This allows why3doc to generate anchors for operator definitions,
including "(*)".