src/HOL/Tools/Sledgehammer/metis_clauses.ML
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-23 blanchet 2010-08-23 use different name for debugging purposes
2010-07-30 blanchet 2010-07-30 don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...
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 "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-07-26 blanchet 2010-07-26 renamed internal function
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-07-21 blanchet 2010-07-21 rename "classrel" to "class_rel"
2010-07-21 blanchet 2010-07-21 rename "combtyp" constructors
2010-07-21 blanchet 2010-07-21 renamed "Literal" to "FOLLiteral"
2010-07-21 blanchet 2010-07-21 renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-30 blanchet 2010-06-30 rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly
2010-06-29 blanchet 2010-06-29 move function
2010-06-29 blanchet 2010-06-29 rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
2010-06-29 blanchet 2010-06-29 move "nice names" from Metis to TPTP format
2010-06-29 blanchet 2010-06-29 move functions not needed by Metis out of "Metis_Clauses"
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 relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer