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