src/HOL/Tools/res_hol_clause.ML
2006-08-02 mengj 2006-08-02 Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
2006-08-01 mengj 2006-08-01 Added in code to check too general axiom clauses.
2006-07-15 mengj 2006-07-15 Only include combinators if required by goals and user specified lemmas. Remove a clause if too general.
2006-07-13 paulson 2006-07-13 "conjecture" must be lower case
2006-07-06 paulson 2006-07-06 some tidying; fixed the output of theorem names
2006-07-05 mengj 2006-07-05 Literals aren't sorted any more.
2006-06-29 paulson 2006-06-29 added the "th" field to datatype Clause
2006-05-29 paulson 2006-05-29 warnings to debug outputs; default translation to const-typed
2006-05-25 mengj 2006-05-25 Changed the DFG format's functions' declaration procedure.
2006-05-25 mengj 2006-05-25 Fixed a bug.
2006-05-25 mengj 2006-05-25 HOL problems now have DFG output format.
2006-04-28 mengj 2006-04-28 changed the functions for getting HOL helper clauses.
2006-04-22 mengj 2006-04-22 Changed the treatment of equalities.
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
2006-04-07 mengj 2006-04-07 tptp_write_file accepts axioms as thm.
2006-03-07 mengj 2006-03-07 Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-02-23 mengj 2006-02-23 Default type level is T_FULL now.
2006-01-30 paulson 2006-01-30 tidy-up of res_clause.ML, removing the "predicates" field
2006-01-20 mengj 2006-01-20 fixed a bug
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-20 mengj 2005-12-20 Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-06 mengj 2005-12-06 Added new type embedding methods for translating HOL clauses.
2005-11-28 mengj 2005-11-28 Added flags for setting and detecting whether a problem needs combinators.
2005-11-18 mengj 2005-11-18 -- terms are fully typed. -- only the top-level boolean terms are predicates.
2005-10-28 mengj 2005-10-28 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.