src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
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