src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
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-14 ago expect SPASS 3.7, and give a friendly warning if an older version is used
2010-05-17 ago generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
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-28 ago reintroduced short names for HOL->FOL constants; other parts of the code rely on these
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-27 ago in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
2010-04-25 ago support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 ago remove some bloat
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 allow "_" in TPTP names in debug mode
2010-04-19 ago get rid of "List.foldl" + add timestamp to SPASS
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-29 ago make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29 ago get rid of Polyhash, since it's no longer used
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