src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
Tue, 29 Jun 2010 10:56:45 +0200 blanchet Sledgehammer can save some msecs by cheating
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
Tue, 22 Jun 2010 18:47:45 +0200 blanchet missing "Unsynchronized" + make exception take a unit
Tue, 22 Jun 2010 14:28:22 +0200 blanchet removed Sledgehammer's support for the DFG syntax;
Mon, 21 Jun 2010 12:31:41 +0200 blanchet try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
Mon, 14 Jun 2010 20:48:36 +0200 blanchet missing case
Fri, 14 May 2010 22:29:50 +0200 blanchet renamed options
Fri, 14 May 2010 11:23:42 +0200 blanchet made Sledgehammer's full-typed proof reconstruction work for the first time;
Sat, 01 May 2010 21:29:03 +0200 krauss made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
Wed, 28 Apr 2010 13:00:30 +0200 blanchet remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
Tue, 27 Apr 2010 17:44:33 +0200 blanchet make Sledgehammer more friendly if no subgoal is left
Mon, 26 Apr 2010 21:20:43 +0200 blanchet introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
Sun, 25 Apr 2010 11:38:46 +0200 blanchet support readable names even when Isar proof reconstruction is enabled -- useful for debugging
Fri, 23 Apr 2010 19:36:49 +0200 blanchet cosmetics
Fri, 23 Apr 2010 19:12:49 +0200 blanchet remove some bloat
Fri, 23 Apr 2010 17:38:25 +0200 blanchet move the minimizer to the Sledgehammer directory
less more (0) tip