Mon, 20 Dec 2010 21:04:45 +0100 boehmes added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
Mon, 20 Dec 2010 08:17:23 +0100 boehmes perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
Sun, 19 Dec 2010 17:55:56 +0100 boehmes only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
Fri, 17 Dec 2010 13:12:58 +0100 wenzelm tuned;
Thu, 16 Dec 2010 12:19:00 +0000 paulson merged
Thu, 16 Dec 2010 12:05:00 +0000 paulson made sml/nj happy
Wed, 15 Dec 2010 18:18:56 +0100 boehmes fixed trigger inference: testing if a theorem already has a trigger was too strict;
Wed, 15 Dec 2010 16:32:45 +0100 boehmes fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
Wed, 15 Dec 2010 08:39:24 +0100 boehmes re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
Wed, 08 Dec 2010 08:33:02 +0100 boehmes be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
Wed, 24 Nov 2010 15:33:35 +0100 boehmes swap names for built-in tester functions (to better reflect the intuition of what they do);
Wed, 24 Nov 2010 13:31:12 +0100 boehmes instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in
Mon, 22 Nov 2010 15:45:43 +0100 boehmes share and use more utility functions;
Wed, 17 Nov 2010 08:14:56 +0100 boehmes 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)
Mon, 08 Nov 2010 12:13:44 +0100 boehmes 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)
Fri, 29 Oct 2010 18:17:10 +0200 boehmes eta-expand built-in constants; also rewrite partially applied natural number terms
Fri, 29 Oct 2010 18:17:09 +0200 boehmes optionally drop assumptions which cannot be preprocessed
Fri, 29 Oct 2010 18:17:05 +0200 boehmes tuned
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
Tue, 26 Oct 2010 11:45:12 +0200 boehmes 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
Tue, 26 Oct 2010 11:39:26 +0200 boehmes keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
Fri, 17 Sep 2010 10:52:35 +0200 boehmes 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
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Tue, 13 Jul 2010 02:29:05 +0200 boehmes fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
Thu, 27 May 2010 16:29:33 +0200 boehmes renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip