src/HOL/ResAtpMethods.thy
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 18201 6c63f0eb16d7
child 19193 45c8db82893d
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;

(* 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