src/HOL/Tools/res_atp_setup.ML
2005-10-28 mengj 2005-10-28 Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other 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").