src/HOL/Tools/SMT/smt_normalize.ML
2010-11-24 boehmes 2010-11-24 swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)
2010-11-24 boehmes 2010-11-24 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-17 boehmes 2010-11-17 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-10-29 boehmes 2010-10-29 eta-expand built-in constants; also rewrite partially applied natural number terms
2010-10-29 boehmes 2010-10-29 optionally drop assumptions which cannot be preprocessed
2010-10-29 boehmes 2010-10-29 tuned
2010-10-29 boehmes 2010-10-29 introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
2010-10-26 boehmes 2010-10-26 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-26 boehmes 2010-10-26 keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
2010-09-17 boehmes 2010-09-17 add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-07-13 boehmes 2010-07-13 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image