src/HOL/Tools/SMT2/z3_new_replay.ML
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