author | wenzelm |
Thu, 10 Nov 2005 20:57:11 +0100 | |
changeset 18145 | 6757627acf59 |
parent 17958 | c0bc47e944de |
child 18201 | 6c63f0eb16d7 |
permissions | -rw-r--r-- |
(* ID: $Id$ Author: Jia Meng, NICTA *) header {* ATP setup (Vampire and E prover) *} theory ResAtpMethods imports Reconstruction uses "Tools/res_atp_setup.ML" "Tools/res_atp_provers.ML" ("Tools/res_atp_methods.ML") begin oracle vampire_oracle ("string list * int") = {* ResAtpProvers.vampire_o *} oracle eprover_oracle ("string list * int") = {* ResAtpProvers.eprover_o *} use "Tools/res_atp_methods.ML" setup ResAtpMethods.ResAtps_setup end