src/HOL/Tools/Sledgehammer/sledgehammer.ML
2010-07-29 ago use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
2010-07-29 ago handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
2010-07-29 ago speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
2010-07-29 ago work around atomization failures
2010-07-29 ago perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
2010-07-29 ago fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
2010-07-29 ago generate correct names for "$true" and "$false";
2010-07-29 ago don't assume canonical rule format
2010-07-29 ago avoid "clause" and "cnf" terminology where it no longer makes sense
2010-07-29 ago "axiom_clauses" -> "axioms" (these are no longer clauses)
2010-07-29 ago remove the "extra_clauses" business introduced in 19a5f1c8a844;
2010-07-28 ago handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
2010-07-28 ago minor refactoring
2010-07-28 ago fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
2010-07-28 ago revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
2010-07-28 ago renaming
2010-07-28 ago improve detection of installed SPASS
2010-07-27 ago minor refactoring
2010-07-27 ago more refactoring
2010-07-27 ago rename "ATP_Manager" ML module to "Sledgehammer";
2010-07-27 ago rename