| Tue, 07 Mar 2006 03:49:26 +0100 | mengj | When ATP methods call ATPs, all input clauses from one subgoal are written to one file. | file | diff | annotate |
| Fri, 18 Nov 2005 07:10:37 +0100 | mengj | -- changed the interface of functions vampire_oracle and eprover_oracle. | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:37 +0200 | wenzelm | proper header; | 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 |