re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure); abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context); proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions); built-in functions carry additionally their arity and their most general type; slightly generalized the definition of fun_app

re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level); added simple trigger inference mechanism; added syntactic checks for triggers and quantifier weights; factored out the normalization of special quantifiers (used to be in the eta-normalization part); normalization now unfolds abs/min/max (not SMT-LIB-specific); rules for pairs and function update are not anymore added automatically to the problem; more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions); normalizations are now managed in a class-based manner (similar to built-in symbols)

added option to enable trigger inference; better documentation of triggers and SMT available options

moved SMT classes and dictionary functions to SMT_Utils

tuned

rewrite Z3 model equations one-by-one (the previous approach led to loss of information)

added option to modify the random seed of SMT solvers

adding an Isar version of the MacLaurin theorem from some students' work in 2005

Admin/contributed_components tries to formalize compatibility with external components (for use e.g. by testing tools), guessing from the content of TUM contrib_devel directory

separated dictionary weakning into separate type

eliminated dest_all_all_ctx

private term variant of Variable.focus

adding an executable THE operator on finite types

tuned headers

added signature; more honest header

add HOLCF library theories with cpo/predomain instances for HOL types

xsymbol notation for powerdomain types

new powerdomain lemmas

made smlnj happy

merged

moved most fundamental lemmas upwards

setting finite_type_size to 1 in mutabelle_extra

adding check_all instances for a few more finite types in smallcheck

removing unneccassary sort constraints

made smlnj happy

merged

tuned names

dictionary constants must permit explicit weakening of classes; tuned names

tracing of term to be evaluated

merged