src/HOL/Tools/Sledgehammer/metis_tactics.ML
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-21 blanchet 2010-06-21 try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-14 blanchet 2010-06-14 A function called "untyped_aconv" shouldn't look at the bound names!
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-12 blanchet 2010-06-12 "raise Fail" for internal errors + one new internal error (instead of "Match")
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-02 blanchet 2010-06-02 give more helpful error message
2010-05-17 blanchet 2010-05-17 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
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-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
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 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-26 blanchet 2010-04-26 adapt code to reflect new signature of "neg_clausify"
2010-04-24 blanchet 2010-04-24 better error reporting; in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs
2010-04-19 blanchet 2010-04-19 added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
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-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
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