src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
2010-05-17 blanchet 2010-05-17 generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process
2010-05-14 blanchet 2010-05-14 renamed two Sledgehammer options
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-04-29 blanchet 2010-04-29 fix more "undeclared symbol" errors related to SPASS's DFG format
2010-04-29 blanchet 2010-04-29 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
2010-04-27 blanchet 2010-04-27 make Sledgehammer more friendly if no subgoal is left
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-25 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory
2010-04-20 blanchet 2010-04-20 fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared; this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated
2010-04-20 blanchet 2010-04-20 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-19 blanchet 2010-04-19 cosmetics
2010-04-19 blanchet 2010-04-19 get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19 blanchet 2010-04-19 got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19 blanchet 2010-04-19 don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19 blanchet 2010-04-19 set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19 blanchet 2010-04-19 get rid of "List.foldl" + add timestamp to SPASS
2010-04-16 blanchet 2010-04-16 restore order of clauses in TPTP output; there's a rather subtle invariant w.r.t. "extract_lemmas"
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-15 blanchet 2010-04-15 give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15 blanchet 2010-04-15 make Sledgehammer's output more debugging friendly
2010-03-23 blanchet 2010-03-23 added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-17 blanchet 2010-03-17 move Sledgehammer files in a directory of their own