src/HOL/Tools/Sledgehammer/clausifier.ML
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-09 blanchet 2010-08-09 replace recursion with "fold"
2010-08-09 blanchet 2010-08-09 remove now needless "Thm.transfer"
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 standardize "Author" tags
2010-07-27 blanchet 2010-07-27 get rid of more dead wood
2010-07-26 blanchet 2010-07-26 prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
2010-07-26 blanchet 2010-07-26 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
2010-07-26 blanchet 2010-07-26 added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-06-29 blanchet 2010-06-29 more elegant cheating
2010-06-29 blanchet 2010-06-29 Sledgehammer can save some msecs by cheating
2010-06-29 blanchet 2010-06-29 move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache
2010-06-28 blanchet 2010-06-28 remove obsolete component of CNF clause tuple (and reorder it)
2010-06-28 blanchet 2010-06-28 get rid of Skolem cache by performing CNF-conversion after fact selection
2010-06-28 blanchet 2010-06-28 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
2010-06-28 blanchet 2010-06-28 always perform relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 factor out thread creation
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)