src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-22 blanchet 2010-06-22 missing "Unsynchronized" + make exception take a unit
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-21 blanchet 2010-06-21 try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-14 blanchet 2010-06-14 missing case
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-05-01 krauss 2010-05-01 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-04-28 blanchet 2010-04-28 remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants
2010-04-27 blanchet 2010-04-27 make Sledgehammer more friendly if no subgoal is left
2010-04-26 blanchet 2010-04-26 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method; the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
2010-04-25 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 blanchet 2010-04-23 cosmetics
2010-04-23 blanchet 2010-04-23 remove some bloat
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory