src/HOL/SMT2.thy
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 added support for CVC4 in SMT2
2014-06-12 blanchet 2014-06-12 don't ask proof-disabled solvers to do proofs
2014-06-12 blanchet 2014-06-12 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-12 blanchet 2014-06-12 eliminate dependency of SMT2 module on 'list'
2014-06-12 blanchet 2014-06-12 use 'ctr_sugar' abstraction in SMT(2)
2014-06-11 blanchet 2014-06-11 factor out SMT-LIB 2 type/term parsing from Z3-specific code
2014-06-11 blanchet 2014-06-11 removed '_new' sufffix in SMT2 solver names (in some cases)
2014-06-03 blanchet 2014-06-03 tune
2014-06-03 blanchet 2014-06-03 removed SMT weights -- their impact was very inconclusive anyway
2014-06-02 blanchet 2014-06-02 refactored Z3 to Isar proof construction code
2014-06-02 blanchet 2014-06-02 split replay and proof parsing for Z3
2014-06-02 blanchet 2014-06-02 removed counterexample parser (obsolete and useless in practice)
2014-03-13 blanchet 2014-03-13 avoid name clash
2014-03-13 blanchet 2014-03-13 move lemmas to theory file, towards textual proof reconstruction
2014-03-13 blanchet 2014-03-13 simpler translation of 'div' and 'mod' for Z3
2014-03-13 blanchet 2014-03-13 tuning
2014-03-13 blanchet 2014-03-13 adapted to renamed ML files
2014-03-13 blanchet 2014-03-13 reintroduced old model reconstruction code -- still needs to be ported
2014-03-13 blanchet 2014-03-13 have Sledgehammer generate Isar proofs from Z3 proofs
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle