src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
2010-06-29 ago move blacklisting completely out of the clausifier;
2010-06-28 ago always perform relevance filtering on original formulas
2010-06-25 ago got rid of "respect_no_atp" option, which even I don't use
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 remove junk
2010-06-25 ago further reduce dependencies on "sledgehammer_fact_filter.ML"
2010-06-25 ago move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
2010-06-25 ago eta-expand
2010-06-25 ago improve the natural formula relevance filter code, so that it behaves more like the CNF one
2010-06-24 ago a76ace919f1c wasn't quite right; second try
2010-06-24 ago make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
2010-06-23 ago improve the new "natural formula" fact filter
2010-06-23 ago fix bug with "skolem_id" + sort facts for increased readability
2010-06-22 ago factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22 ago missing "Unsynchronized" + make exception take a unit
2010-06-22 ago added code to optionally perform fact filtering on the original (non-CNF) formulas
2010-06-22 ago more cosmetics
2010-06-22 ago cosmetics + prevent consideration of inlined Skolem terms in relevance filter
2010-06-22 ago canonical argument order
2010-06-22 ago leverage new data structure for handling "add:" and "del:"
2010-06-22 ago thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
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 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 ago proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-07 ago made SML/NJ happy again;
2010-06-05 ago renaming
2010-06-05 ago show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 ago make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
2010-06-05 ago totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
2010-05-28 ago make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-17 ago make sure chained facts don't pop up in the metis proof
2010-05-14 ago renamed two Sledgehammer options
2010-05-05 ago 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-28 ago make sure short theorem names are preferred to composite ones in Sledgehammer;
2010-04-27 ago remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-25 ago support readable names even when Isar proof reconstruction is enabled -- useful for debugging
2010-04-19 ago make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19 ago rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-16 ago optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
2010-04-16 ago reorganize Sledgehammer's relevance filter slightly
2010-03-29 ago remove use of Polyhash;
2010-03-29 ago reintroduce efficient set structure to collect "no_atp" theorems
2010-03-29 ago made "theory_const" a Sledgehammer option;
2010-03-29 ago added "respect_no_atp" and "convergence" options to Sledgehammer;
2010-03-24 ago revert debugging output that shouldn't have been submitted in the first place
2010-03-24 ago honor the newly introduced Sledgehammer parameters and fixed the parsing;
2010-03-23 ago added options to Sledgehammer;
2010-03-19 ago more Sledgehammer refactoring
2010-03-18 ago now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 ago renamed Sledgehammer structures
2010-03-17 ago move Sledgehammer files in a directory of their own