src/HOL/SMT_Examples/SMT_Word_Examples.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-18 blanchet 2014-09-18 renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-03-13 blanchet 2014-03-13 updated SMT example certificates
2014-03-13 blanchet 2014-03-13 use 'smt2' in SMT examples as much as currently possible
2014-03-11 blanchet 2014-03-11 full path
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2011-01-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2010-12-19 boehmes 2010-12-19 updated SMT certificates
2010-11-12 boehmes 2010-11-12 look for certificates relative to the theory
2010-10-26 boehmes 2010-10-26 changed SMT configuration options; updated SMT certificates
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable