Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added in SPASS oracle.
authormengj
Thu, 25 May 2006 11:50:55 +0200
changeset 19721 515f660c0ccb
parent 19720 f68f6f958a1d
child 19722 e7a5b54248bc
Added in SPASS oracle.
src/HOL/ResAtpMethods.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle