src/HOL/SMT_Examples/SMT_Tests.certs
2012-03-27 boehmes 2012-03-27 dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
2012-03-26 blanchet 2012-03-26 reintroduced broken proofs and regenerated certificates
2011-12-25 haftmann 2011-12-25 updated certificate
2011-09-14 boehmes 2011-09-14 observe distinction between sets and predicates
2011-09-06 boehmes 2011-09-06 added some examples for pattern and weight annotations
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-03-09 boehmes 2011-03-09 finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
2011-01-03 boehmes 2011-01-03 updated SMT certificates
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-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-29 boehmes 2010-10-29 updated SMT certificates
2010-10-26 boehmes 2010-10-26 changed SMT configuration options; updated SMT certificates
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 added function update examples and set examples
2010-05-27 boehmes 2010-05-27 updated SMT certificates
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