| Fri, 28 Oct 2005 02:27:19 +0200 | mengj | Added new functions to handle HOL goals and lemmas. | changeset | files |
| Fri, 28 Oct 2005 02:25:57 +0200 | mengj | 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. | changeset | files |
| Fri, 28 Oct 2005 02:24:58 +0200 | mengj | Added several functions to the signature. | changeset | files |