src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
2010-08-23 blanchet 2010-08-23 prevent double inclusion of the fact "True_or_False" in TPTP problems
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-20 blanchet 2010-08-20 remove trivial facts
2010-08-20 blanchet 2010-08-20 use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; avoids relying on inconsistently implemented feature of TPTP format
2010-08-20 blanchet 2010-08-20 transform elim theorems before filtering "bool" and "prop" variables out; another consequence of the transition to FOF
2010-08-20 blanchet 2010-08-20 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF
2010-08-19 blanchet 2010-08-19 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 blanchet 2010-08-19 fix atomize
2010-08-19 blanchet 2010-08-19 improve atomization
2010-08-18 blanchet 2010-08-18 added "max_relevant_per_iter" option to Sledgehammer
2010-08-18 blanchet 2010-08-18 handle bound name conflicts gracefully in FOF translation
2010-08-17 blanchet 2010-08-17 repair translation of "c_fequal"
2010-08-17 blanchet 2010-08-17 invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms; this resulted in a subtle soundness bug in Sledgehammer -- introduced by the transition to FOF
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)