src/HOL/Tools/res_hol_clause.ML
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.