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