author | wenzelm |
Thu, 16 Feb 2006 18:25:54 +0100 | |
changeset 19070 | 99001616e0e2 |
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