src/HOL/ResAtpMethods.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18201 6c63f0eb16d7
child 19193 45c8db82893d
permissions -rw-r--r--
adaptions to codegen_package
     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_setup.ML"
    11   "Tools/res_atp_provers.ML"
    12   ("Tools/res_atp_methods.ML")
    13 
    14 begin
    15 
    16 oracle vampire_oracle ("(string list * string list) * int") = {* ResAtpProvers.vampire_o *}
    17 oracle eprover_oracle ("(string list * string list) * int") = {* ResAtpProvers.eprover_o *}
    18 
    19 use "Tools/res_atp_methods.ML"
    20 setup ResAtpMethods.ResAtps_setup
    21 
    22 end