src/HOL/Tools/SMT2/smt2_solver.ML
Mon, 02 Jun 2014 17:34:26 +0200 blanchet simplified counterexample handling
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)
Fri, 16 May 2014 19:13:50 +0200 blanchet honor original format of conjecture or hypotheses in Z3-to-Isar proofs
Fri, 14 Mar 2014 12:09:51 +0100 blanchet delayed construction of command (and of noncommercial check) + tuning
Fri, 14 Mar 2014 11:52:03 +0100 blanchet tuning
Fri, 14 Mar 2014 11:15:46 +0100 blanchet undo rewrite rules (e.g. for 'fun_app') in Isar
Fri, 14 Mar 2014 11:05:37 +0100 blanchet tuning
Thu, 13 Mar 2014 16:21:09 +0100 blanchet updated SMT2 examples and certificates
Thu, 13 Mar 2014 14:48:20 +0100 blanchet simplify index handling
Thu, 13 Mar 2014 14:48:20 +0100 blanchet correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
Thu, 13 Mar 2014 13:18:14 +0100 blanchet thread through step IDs from Z3 to Sledgehammer
Thu, 13 Mar 2014 13:18:14 +0100 blanchet avoid names that may clash with Z3's output (e.g. '')
Thu, 13 Mar 2014 13:18:14 +0100 blanchet let exception pass through in debug mode
Thu, 13 Mar 2014 13:18:14 +0100 blanchet adapted to renamed ML files
Thu, 13 Mar 2014 13:18:13 +0100 blanchet slacker error code policy for Z3
Thu, 13 Mar 2014 13:18:13 +0100 blanchet repaired 'if' logic
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 tuned ML interface
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
less more (0) tip