src/HOL/ResAtpMethods.thy
author mengj
Wed Oct 19 06:33:24 2005 +0200 (2005-10-19)
changeset 17905 1574533861b1
child 17907 c20e4bddcb11
permissions -rw-r--r--
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj@17905
     1
(* ID: $Id$
mengj@17905
     2
   Author: Jia Meng
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@17905
     8
  imports Reconstruction ResAtpOracle
mengj@17905
     9
mengj@17905
    10
  uses "Tools/res_atp_setup.ML"
mengj@17905
    11
       "Tools/res_atp_methods.ML"
mengj@17905
    12
mengj@17905
    13
begin
mengj@17905
    14
setup ResAtpMethods.ResAtps_setup
mengj@17905
    15
mengj@17905
    16
end