src/HOL/SMT_Examples/SMT_Examples.certs
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2015-12-04 blanchet 2015-12-04 updated SMT certificates
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-04-08 blanchet 2015-04-08 updated certificates to latest Z3 (and took out one problem that no longer works)
2014-11-24 blanchet 2014-11-24 updated SMT certificates
2014-09-24 blanchet 2014-09-24 updated SMT certificates
2014-09-18 blanchet 2014-09-18 renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-04-25 blanchet 2014-04-25 use Z3 4.3.2 to fix most FIXMEs
2014-03-13 blanchet 2014-03-13 updated SMT2 certificates
2014-03-13 blanchet 2014-03-13 use 'smt2' in SMT examples as much as currently possible
2014-02-12 blanchet 2014-02-12 updated certificates
2013-09-24 blanchet 2013-09-24 updated certificates
2013-03-28 boehmes 2013-03-28 re-generated SMT certificates
2013-01-01 blanchet 2013-01-01 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
2012-11-01 blanchet 2012-11-01 regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
2012-03-26 blanchet 2012-03-26 reintroduced broken proofs and regenerated certificates
2012-01-03 blanchet 2012-01-03 regenerate SMT example certificates, to reflect "set" type constructor
2011-11-07 boehmes 2011-11-07 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
2011-07-18 boehmes 2011-07-18 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
2011-06-26 boehmes 2011-06-26 updated SMT certificates
2011-06-08 boehmes 2011-06-08 updated SMT certificates
2011-06-05 boehmes 2011-06-05 updated SMT certificates
2011-05-31 boehmes 2011-05-31 updated SMT certificates
2011-04-08 boehmes 2011-04-08 added SMT certificates
2011-04-08 boehmes 2011-04-08 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
2011-02-21 boehmes 2011-02-21 added test cases with quantifier occurring in first-order term positions
2011-02-14 boehmes 2011-02-14 limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate
2010-12-20 boehmes 2010-12-20 updated SMT certificates
2010-12-19 boehmes 2010-12-19 updated SMT certificates
2010-12-17 boehmes 2010-12-17 updated SMT certificates
2010-12-17 boehmes 2010-12-17 updated SMT certificates
2010-12-15 boehmes 2010-12-15 updated SMT certificates
2010-12-07 boehmes 2010-12-07 updated SMT certificates
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-03 boehmes 2010-11-03 updated SMT certificates
2010-10-26 boehmes 2010-10-26 changed SMT configuration options; updated SMT certificates
2010-05-27 boehmes 2010-05-27 updated SMT certificates
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27 boehmes 2010-05-27 use Z3's builtin support for div and mod
2010-05-26 boehmes 2010-05-26 updated SMT certificates
2010-05-12 boehmes 2010-05-12 updated SMT certificates