src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
2010-09-27 blanchet 2010-09-27 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-20 wenzelm 2010-09-20 added XML.content_of convenience -- cover XML.body, which is the general situation;
2010-09-17 blanchet 2010-09-17 move functions around
2010-09-16 blanchet 2010-09-16 avoid code duplication
2010-09-14 blanchet 2010-09-14 speed up helper function
2010-09-11 blanchet 2010-09-11 implemented Auto Sledgehammer
2010-08-26 blanchet 2010-08-26 improve SPASS hack, when a clause comes from several facts
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-24 blanchet 2010-08-24 clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name
2010-08-24 blanchet 2010-08-24 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-20 blanchet 2010-08-20 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF
2010-08-05 blanchet 2010-08-05 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-07-28 blanchet 2010-07-28 minor refactoring
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