| 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. | file | diff | annotate |
| Wed, 19 Oct 2005 10:25:46 +0200 | mengj | *** empty log message *** | file | diff | annotate |
| Wed, 19 Oct 2005 06:33:24 +0200 | mengj | Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). | file | diff | annotate |