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
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 header {* ATP setup (Vampire and E prover) *}
     6 
     7 theory ResAtpMethods
     8 imports Reconstruction
     9 uses
    10   "Tools/res_atp_provers.ML"
    11   ("Tools/res_atp_methods.ML")
    12 
    13 begin
    14 
    15 oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
    16 oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
    17 
    18 use "Tools/res_atp_methods.ML"
    19 setup ResAtpMethods.ResAtps_setup
    20 
    21 end