src/HOL/Tools/Sledgehammer/clausifier.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 transform elim theorems before filtering "bool" and "prop" variables out;
2010-08-20 ago beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
2010-08-09 ago move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-09 ago replace recursion with "fold"
2010-08-09 ago remove now needless "Thm.transfer"
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 prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
2010-07-26 ago reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
2010-07-26 ago added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
2010-07-26 ago generate full first-order formulas (FOF) in Sledgehammer
2010-06-29 ago more elegant cheating
2010-06-29 ago Sledgehammer can save some msecs by cheating
2010-06-29 ago move blacklisting completely out of the clausifier;
2010-06-28 ago remove obsolete component of CNF clause tuple (and reorder it)
2010-06-28 ago get rid of Skolem cache by performing CNF-conversion after fact selection
2010-06-28 ago always perform "inline" skolemization, polymorphism or not, Skolem cache or not
2010-06-28 ago always perform relevance filtering on original formulas
2010-06-25 ago factor out thread creation
2010-06-25 ago renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";