src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
2010-06-22 ago reintroduce new Sledgehammer polymorphic handling code;
2010-06-21 ago try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-15 ago found missing beta-eta-contraction
2010-06-14 ago expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-14 ago adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 ago proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-05-17 ago generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-14 ago renamed two Sledgehammer options
2010-05-14 ago made Sledgehammer's full-typed proof reconstruction work for the first time;
2010-04-29 ago fix more "undeclared symbol" errors related to SPASS's DFG format
2010-04-29 ago 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 ago make Sledgehammer more friendly if no subgoal is left
2010-04-26 ago introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
2010-04-25 ago support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 ago move the minimizer to the Sledgehammer directory
2010-04-20 ago fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
2010-04-20 ago 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 ago cosmetics
2010-04-19 ago 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 ago got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19 ago don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19 ago set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19 ago get rid of "List.foldl" + add timestamp to SPASS
2010-04-16 ago restore order of clauses in TPTP output;
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-15 ago give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15 ago make Sledgehammer's output more debugging friendly
2010-03-23 ago added options to Sledgehammer;
2010-03-19 ago more Sledgehammer refactoring
2010-03-17 ago renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17 ago renamed Sledgehammer structures
2010-03-17 ago move Sledgehammer files in a directory of their own