made SML/NJ happy;

merged

added SMT certificates

use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)

fixed eta-expansion: use correct order to apply new bound variables

check if negating the goal is possible (avoids CTERM exception for Pure propositions)

unfold and eta-contract let expressions before lambda-lifting to avoid bad terms

corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables

merged

deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments

generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations

correcting constant name in exhaustive_generators

switching fast compilation off by default for now in exhaustive quickcheck

ensuring datatype limitations before the instantiation in quickcheck_exhaustive

rational and real instances for new compilation scheme for exhaustive quickcheck

splitting exhaustive and full_exhaustive into separate type classes

removing duplicate code

revisiting mk_equation functions and refactoring them in exhaustive quickcheck

creating a general mk_equation_terms for the different compilations

adding an even faster compilation scheme

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

tuned;

present type variables; tuned;

unparse: more accurate markup for syntax consts, notably binders;

notation: proper markup for type constructor / constant;

tuned signature;

more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;