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