Wed, 09 Nov 2005 18:01:33 +0100 | paulson | Skolemization by inference, but not quite finished | file | diff | annotate |
Thu, 03 Nov 2005 04:31:12 +0100 | mengj | Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names. | file | diff | annotate |
Fri, 28 Oct 2005 17:27:49 +0200 | haftmann | circumvented smlnj value restriction | file | diff | annotate |
Fri, 28 Oct 2005 02:27:19 +0200 | mengj | Added new functions to handle HOL goals and lemmas. | file | diff | annotate |
Fri, 21 Oct 2005 02:57:22 +0200 | mengj | Merged theory ResAtpOracle.thy into ResAtpMethods.thy | 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 |