src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-07-23 blanchet 2010-07-23 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.
2010-06-25 blanchet 2010-06-25 exploit "Name.desymbolize" to remove some dependencies
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-14 blanchet 2010-06-14 expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-02 blanchet 2010-06-02 honor "xsymbols"
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-29 blanchet 2010-04-29 expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute
2010-04-28 blanchet 2010-04-28 parentheses around nested cases
2010-04-28 blanchet 2010-04-28 unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28 blanchet 2010-04-28 support Vampire definitions of constants as "let" constructs in Isar proofs
2010-04-27 blanchet 2010-04-27 fix types of "fix" variables to help proof reconstruction and aid readability
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-23 blanchet 2010-04-23 remove some bloat
2010-04-16 blanchet 2010-04-16 Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16 blanchet 2010-04-16 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16 blanchet 2010-04-16 store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-14 blanchet 2010-04-14 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used
2010-03-23 blanchet 2010-03-23 added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional