src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
Mon, 09 Dec 2013 06:33:46 +0100 blanchet adapted code for Z3 proof reconstruction
Tue, 19 Nov 2013 18:38:25 +0100 blanchet tuning
Fri, 20 Sep 2013 22:39:30 +0200 blanchet merged "isar_try0" and "isar_minimize" options
Tue, 13 Aug 2013 10:26:56 +0200 blanchet Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
Fri, 12 Jul 2013 22:41:25 +0200 smolkas added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
Fri, 12 Jul 2013 19:03:08 +0200 smolkas cleaner preplay interface
Fri, 12 Jul 2013 14:18:06 +0200 smolkas minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
less more (0) tip