# HG changeset patch
# User wenzelm
# Date 1129911277 -7200
# Node ID c0bc47e944de4d40514226cd979506e73ab58a2c
# Parent  d31acb64aa9a4e4dc733a70b2c8d3d1ec7a22e1d
proper header;
proper use of ML files;

diff -r d31acb64aa9a -r c0bc47e944de src/HOL/ResAtpMethods.thy
--- a/src/HOL/ResAtpMethods.thy	Fri Oct 21 18:14:36 2005 +0200
+++ b/src/HOL/ResAtpMethods.thy	Fri Oct 21 18:14:37 2005 +0200
@@ -1,26 +1,22 @@
 (* ID: $Id$
    Author: Jia Meng, NICTA
- a method to setup "vampire" method 
- a method to setup "eprover" method
 *)
 
-theory ResAtpMethods
-  imports Reconstruction 
+header {* ATP setup (Vampire and E prover) *}
 
-uses ("Tools/res_atp_setup.ML")
-     ("Tools/res_atp_provers.ML")
-     ("Tools/res_atp_methods.ML")
+theory ResAtpMethods
+imports Reconstruction
+uses
+  "Tools/res_atp_setup.ML"
+  "Tools/res_atp_provers.ML"
+  ("Tools/res_atp_methods.ML")
 
 begin
 
-ML{*use "Tools/res_atp_setup.ML"*}
-ML{*use "Tools/res_atp_provers.ML"*}
-
-oracle vampire_oracle ("string list * int") =  {*ResAtpProvers.vampire_o*}
-oracle eprover_oracle ("string list * int") =  {*ResAtpProvers.eprover_o*}
+oracle vampire_oracle ("string list * int") = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle ("string list * int") = {* ResAtpProvers.eprover_o *}
 
-
-ML{*use "Tools/res_atp_methods.ML"*}
+use "Tools/res_atp_methods.ML"
+setup ResAtpMethods.ResAtps_setup
 
-setup ResAtpMethods.ResAtps_setup
 end