src/HOL/ResAtpMethods.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 19193 45c8db82893d
child 19721 515f660c0ccb
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
mengj@17905
     1
(* ID: $Id$
mengj@17907
     2
   Author: Jia Meng, NICTA
mengj@17905
     3
*)
mengj@17905
     4
wenzelm@17958
     5
header {* ATP setup (Vampire and E prover) *}
mengj@17905
     6
wenzelm@17958
     7
theory ResAtpMethods
wenzelm@17958
     8
imports Reconstruction
wenzelm@17958
     9
uses
wenzelm@17958
    10
  "Tools/res_atp_provers.ML"
wenzelm@17958
    11
  ("Tools/res_atp_methods.ML")
mengj@17905
    12
mengj@17905
    13
begin
mengj@17939
    14
mengj@19193
    15
oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
mengj@19193
    16
oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
mengj@17939
    17
wenzelm@17958
    18
use "Tools/res_atp_methods.ML"
wenzelm@17958
    19
setup ResAtpMethods.ResAtps_setup
mengj@17939
    20
mengj@17907
    21
end