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

Theory names are assumed to be unique with respect to their path.
Therefore, do not attempt to disambiguate them, which should result
in more readable / predictable names.

the name of the projection to projected element.

Model elements in source code line are represented as list of JSON objects
with attributes "name", "value", and "kind". The attribute "name" is a
name of a counterexample element, the attribute "value" is the value of
the counterexample element, and the attribute "kind" is the kind of
counterexample element, currently one of "old", "result", "error_message",
and "other".

This fixes (-2) mod 2 being evaluated as nonzero.

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false

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

To do so, add "overriding" keyword in front of "syntax" in the driver file as in, e.g.,
  overriding syntax function to_uint "(bv2int %1)"

One can only have one overriding for a specific function/type.

Prevent loosing labels of formulas with f.t_node equal to Tquant in
transformations eliminate_algebraic and introduce_premises.

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

The concatenation of strings in the list of strings returned by
bounded_split must be equal to the string being split.