more detailed tracing; tuned;

defensive Term_Sharing, to avoid extending trusted code base of inference kernel;

more precise parse_name according to XML standard; tuned performance;

explicit structure ML_System; tunned ML bootstrap;

defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);

tuned;

merged

dropped errorneous hint

moved some lemmas

merged

ereal is a complete_linorder instance

class complete_linorder

make "concealed" lambda translation sound

deactivating all quickcheck invocations until parallel invocation works safely

adapting two examples in Predicate_Compile_Examples

use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned

merge

Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal

add code generator setup and tests for ereal

removed debugging facilities accidentally left in the committed code

more precise dependencies

merged

generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)

moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

removed old (unused) SMT monomorphizer

added UNION

merged

rename Fin to enat

add ereal to typeclass infinity

add nat => enat coercion