src/HOL/Tools/res_hol_clause.ML
Tue, 20 Dec 2005 04:29:25 +0100 mengj Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
Tue, 06 Dec 2005 06:21:07 +0100 mengj Added new type embedding methods for translating HOL clauses.
Mon, 28 Nov 2005 07:17:07 +0100 mengj Added flags for setting and detecting whether a problem needs combinators.
Fri, 18 Nov 2005 07:10:00 +0100 mengj -- terms are fully typed.
Fri, 28 Oct 2005 02:23:49 +0200 mengj 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.
less more (0) tip