
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




