src/HOL/SMT2.thy
Tue, 03 Jun 2014 16:02:42 +0200 blanchet tune
Tue, 03 Jun 2014 11:43:07 +0200 blanchet removed SMT weights -- their impact was very inconclusive anyway
Mon, 02 Jun 2014 17:34:27 +0200 blanchet refactored Z3 to Isar proof construction code
Mon, 02 Jun 2014 17:34:26 +0200 blanchet split replay and proof parsing for Z3
Mon, 02 Jun 2014 17:34:25 +0200 blanchet removed counterexample parser (obsolete and useless in practice)
Thu, 13 Mar 2014 14:48:20 +0100 blanchet avoid name clash
Thu, 13 Mar 2014 14:48:20 +0100 blanchet move lemmas to theory file, towards textual proof reconstruction
Thu, 13 Mar 2014 14:48:05 +0100 blanchet simpler translation of 'div' and 'mod' for Z3
Thu, 13 Mar 2014 13:18:14 +0100 blanchet tuning
Thu, 13 Mar 2014 13:18:14 +0100 blanchet adapted to renamed ML files
Thu, 13 Mar 2014 13:18:13 +0100 blanchet reintroduced old model reconstruction code -- still needs to be ported
Thu, 13 Mar 2014 13:18:13 +0100 blanchet have Sledgehammer generate Isar proofs from Z3 proofs
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
less more (0) tip