This reverts commit 98f2682f.

For the moment, new API functions are introduced. If existing API
functions are called, the why3server is not used.

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

Theory int.Exponentiation currently cannot be realized as it includes an
abstract type (only instances of this theory can be realized); no need
to create an file int/Exponentiation.xml.

Works both with Isabelle 2014 and 2015

Issue: stack overflow when loading the driver, how can it be??

Need to compile Alt-Ergo with Nums instead of Zarith,
which is not supported by js_of_ocaml

compile it with make src/trywhy3/trywhy3.js

run it by loading src/trywhy3/index.html in your favorite browser

first issue to solve : loading of standard library

triggering VC.

- Transformation intro_vc_vars_counterexamp introduces new constant with
model labels for every variable in the term that trigger VC and axiom
that this constant is equal to the variable, finds the position of the
term that trigger VC, and saves this position in meta (for smtv2
printer).

- Transformation prepare_for_counterexmp additionally performs the
transformation intro_vc_vars_counterexamp

- smtv2 printer no longer collects the location of the term that
triggers VC and does not collect variables in this term in a special
way. Note that this functionality was not yet completely removed from
the printer. It will be done so after the transformation
intro_vc_vars_counterexmp will be tested.

The rationale:
Variables that should be displayed in counterexample are marked
by model labels ("model", "model_projected", "model_trace:*").

Variables inside the term that triggers VC should be displayed in
counterexample for that VC. However, many VCs (tasks) can be generated
for  a signle *.mlw file and only variables in the term that trigger
the VC (task) that is currently proven should be displayed. That means
that the process of selecting variables inside the term that triggers
VC for counterexample must be done while processing the task. It is
done by transformation intro_vc_vars_counterexmp. This means that smtv2
printer no longer has to find the position of the term that triggers
VC and no longer has to collect variables in this term in a special
way.