# HG changeset patch
# User mengj
# Date 1148550655 -7200
# Node ID 515f660c0ccb258cb468c8f6593058acf9d55b2d
# Parent  f68f6f958a1d99ef9fd662859028e04eacdbec3e
Added in SPASS oracle.

diff -r f68f6f958a1d -r 515f660c0ccb src/HOL/ResAtpMethods.thy
--- a/src/HOL/ResAtpMethods.thy	Thu May 25 08:09:10 2006 +0200
+++ b/src/HOL/ResAtpMethods.thy	Thu May 25 11:50:55 2006 +0200
@@ -2,7 +2,7 @@
    Author: Jia Meng, NICTA
 *)
 
-header {* ATP setup (Vampire and E prover) *}
+header {* ATP setup (Vampire, E prover and SPASS) *}
 
 theory ResAtpMethods
 imports Reconstruction
@@ -14,6 +14,7 @@
 
 oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
 oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
+oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
 
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.ResAtps_setup