2006-03-07 mengj 2006-03-07 When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2005-11-18 mengj 2005-11-18 -- changed the interface of functions vampire_oracle and eprover_oracle.
2005-10-21 wenzelm 2005-10-21 proper header; proper use of ML files;
2005-10-21 mengj 2005-10-21 Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-19 mengj 2005-10-19 *** empty log message ***
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").