--- 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