src/HOL/Tools/Sledgehammer/metis_tactics.ML
2010-08-23 ago perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
2010-08-22 ago treat "using X by metis" (more or less) the same as "by (metis X)"
2010-08-20 ago temporarily disable "fequal" handling in Metis;
2010-08-20 ago merged
2010-08-19 ago encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
2010-08-19 ago use antiquotations for remaining unqualified constants in HOL
2010-08-16 ago Geoff's formatter now needs closed formulas
2010-08-09 ago replace recursion with "fold"
2010-07-29 ago use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
2010-07-29 ago fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
2010-07-29 ago revert exception throwing in FOL_SOLVE, since they're not caught anyway
2010-07-27 ago minor refactoring
2010-07-27 ago standardize "Author" tags
2010-07-27 ago get rid of more dead wood
2010-07-26 ago make TPTP generator accept full first-order formulas
2010-07-26 ago renamed internal function
2010-07-21 ago revert code that was submitted by mistake
2010-07-21 ago renamings + only need second component of name pool to reconstruct proofs
2010-07-21 ago rename "classrel" to "class_rel"
2010-07-21 ago rename "combtyp" constructors
2010-07-21 ago renamed "Literal" to "FOLLiteral"
2010-06-30 ago rewrote the TPTP problem generation code more or less from scratch;
2010-06-29 ago move function
2010-06-29 ago Sledgehammer can save some msecs by cheating
2010-06-29 ago move blacklisting completely out of the clausifier;
2010-06-29 ago rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
2010-06-29 ago move functions not needed by Metis out of "Metis_Clauses"
2010-06-28 ago killed "expand_defs_tac";
2010-06-25 ago renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 ago merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 ago renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
2010-06-25 ago fewer dependencies
2010-06-25 ago more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
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