| Fri, 28 Oct 2005 02:28:20 +0200 | mengj | Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals. | changeset | files |
| 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 |