diff -r 21c6894b5998 -r 1574533861b1 src/HOL/ResAtpOracle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ResAtpOracle.thy	Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,28 @@
+(* ID: $Id$
+   Author: Jia Meng
+
+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
\ No newline at end of file