src/HOL/Tools/SMT2/z3_new_replay.ML
Thu, 10 Jul 2014 18:08:21 +0200 blanchet lambda-lifting for Z3 Isar proofs
Thu, 12 Jun 2014 01:00:49 +0200 blanchet eliminate dependency of SMT2 module on 'list'
Thu, 12 Jun 2014 01:00:49 +0200 blanchet tuning
Wed, 11 Jun 2014 19:15:55 +0200 blanchet tuned code
Wed, 11 Jun 2014 19:15:54 +0200 blanchet factor out SMT-LIB 2 type/term parsing from Z3-specific code
Tue, 03 Jun 2014 11:43:07 +0200 blanchet removed SMT weights -- their impact was very inconclusive anyway
Tue, 03 Jun 2014 10:35:51 +0200 blanchet make SMT code less dependent on Z3 proofs
Mon, 02 Jun 2014 17:34:26 +0200 blanchet split replay and proof parsing for Z3
Thu, 01 May 2014 22:57:34 +0200 boehmes use internal proof-producing SAT solver for more efficient SMT proof replay
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
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 do less work in 'filter' mode
Thu, 13 Mar 2014 13:18:14 +0100 blanchet adapted to renamed ML files
Thu, 13 Mar 2014 13:18:13 +0100 blanchet renamed ML files
less more (0) tip