author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 18201 | 6c63f0eb16d7 |
child 19193 | 45c8db82893d |
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 * string list) * int") = {* ResAtpProvers.vampire_o *} oracle eprover_oracle ("(string list * string list) * int") = {* ResAtpProvers.eprover_o *} use "Tools/res_atp_methods.ML" setup ResAtpMethods.ResAtps_setup end