author | wenzelm |
Wed, 08 Nov 2006 13:48:29 +0100 | |
changeset 21243 | afffe1f72143 |
parent 19721 | 515f660c0ccb |
permissions | -rw-r--r-- |
(* ID: $Id$ Author: Jia Meng, NICTA *) header {* ATP setup (Vampire, E prover and SPASS) *} theory ResAtpMethods imports Reconstruction uses "Tools/res_atp_provers.ML" ("Tools/res_atp_methods.ML") begin 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 end