src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
2010-06-14 ago expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-02 ago honor "xsymbols"
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-04-29 ago expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-28 ago parentheses around nested cases
2010-04-28 ago unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28 ago support Vampire definitions of constants as "let" constructs in Isar proofs
2010-04-27 ago fix types of "fix" variables to help proof reconstruction and aid readability
2010-04-26 ago introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
2010-04-23 ago remove some bloat
2010-04-16 ago Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16 ago added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16 ago store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-14 ago make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-03-29 ago get rid of Polyhash, since it's no longer used
2010-03-23 ago added options to Sledgehammer;