mengj [Fri, 28 Oct 2005 02:27:19 +0200] rev 18001
Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
mengj [Fri, 28 Oct 2005 02:25:57 +0200] rev 18000
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
Also added function "repeat_RS" to the signature.
mengj [Fri, 28 Oct 2005 02:24:58 +0200] rev 17999
Added several functions to the signature.
Added two new functions, which are used by res_hol_clause.ML programs.
mengj [Fri, 28 Oct 2005 02:23:49 +0200] rev 17998
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.