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-05 haftmann 2010-05-05 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 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-28 blanchet 2010-04-28 reintroduced short names for HOL->FOL constants; other parts of the code rely on these
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-27 blanchet 2010-04-27 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 blanchet 2010-04-25 support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-23 blanchet 2010-04-23 remove some bloat
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 allow "_" in TPTP names in debug mode
2010-04-19 blanchet 2010-04-19 get rid of "List.foldl" + add timestamp to SPASS
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-29 blanchet 2010-03-29 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used
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