diff -r 6c20fae2416c -r 3925ab7b8a18 src/HOL/ResAtpOracle.thy --- a/src/HOL/ResAtpOracle.thy Wed Oct 19 21:53:34 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* ID: $Id$ - Author: Jia Meng, NICTA - -setup vampire prover as an oracle -setup E prover as an oracle -*) - -theory ResAtpOracle - imports HOL -uses "Tools/res_atp_setup.ML" - "Tools/res_atp_provers.ML" - -begin - - - - -oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o -*} - - - - -oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o - *} - - -end