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