src/HOL/Tools/Sledgehammer/metis_tactics.ML
2010-06-25 ago move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
2010-06-24 ago make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
2010-06-24 ago make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
2010-06-23 ago have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
2010-06-22 ago factor out TPTP format output into file of its own, to facilitate further changes
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 A function called "untyped_aconv" shouldn't look at the bound names!
2010-06-14 ago adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-12 ago "raise Fail" for internal errors + one new internal error (instead of "Match")
2010-06-11 ago proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-02 ago give more helpful error message
2010-05-17 ago 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 ago generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-15 ago less pervasive names from structure Thm;
2010-05-14 ago made Sledgehammer's full-typed proof reconstruction work for the first time;
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-26 ago adapt code to reflect new signature of "neg_clausify"
2010-04-24 ago better error reporting;
2010-04-19 ago added warning about inconsistent context to Metis;
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-03-28 ago static defaults for configuration options;
2010-03-19 ago more Sledgehammer refactoring
2010-03-17 ago renamed Sledgehammer structures
2010-03-17 ago move Sledgehammer files in a directory of their own