src/HOL/ResAtpMethods.thy
author mengj
Fri Oct 21 02:57:22 2005 +0200 (2005-10-21)
changeset 17939 3925ab7b8a18
parent 17907 c20e4bddcb11
child 17958 c0bc47e944de
permissions -rw-r--r--
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
mengj@17905
     1
(* ID: $Id$
mengj@17907
     2
   Author: Jia Meng, NICTA
mengj@17905
     3
 a method to setup "vampire" method 
mengj@17905
     4
 a method to setup "eprover" method
mengj@17905
     5
*)
mengj@17905
     6
mengj@17905
     7
theory ResAtpMethods
mengj@17939
     8
  imports Reconstruction 
mengj@17905
     9
mengj@17939
    10
uses ("Tools/res_atp_setup.ML")
mengj@17939
    11
     ("Tools/res_atp_provers.ML")
mengj@17939
    12
     ("Tools/res_atp_methods.ML")
mengj@17905
    13
mengj@17905
    14
begin
mengj@17939
    15
mengj@17939
    16
ML{*use "Tools/res_atp_setup.ML"*}
mengj@17939
    17
ML{*use "Tools/res_atp_provers.ML"*}
mengj@17905
    18
mengj@17939
    19
oracle vampire_oracle ("string list * int") =  {*ResAtpProvers.vampire_o*}
mengj@17939
    20
oracle eprover_oracle ("string list * int") =  {*ResAtpProvers.eprover_o*}
mengj@17939
    21
mengj@17939
    22
mengj@17939
    23
ML{*use "Tools/res_atp_methods.ML"*}
mengj@17939
    24
mengj@17939
    25
setup ResAtpMethods.ResAtps_setup
mengj@17907
    26
end