# HG changeset patch
# User wenzelm
# Date 1126973482 -7200
# Node ID 47f7bddc32398461f09f0f226ef09930e8999724
# Parent  83f1dd9d901da2bcdf0127e7b47bbf12d983ef1f
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);

diff -r 83f1dd9d901d -r 47f7bddc3239 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Sat Sep 17 18:11:21 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Sat Sep 17 18:11:22 2005 +0200
@@ -4,34 +4,31 @@
     Copyright   2004  University of Cambridge
 *)
 
-header{*Attributes for Reconstructing External Resolution Proofs*}
+header{* Reconstructing external resolution proofs *}
 
 theory Reconstruction
-    imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
-    uses "Tools/res_lib.ML"
+imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
+uses "Tools/res_lib.ML"
 
-	 "Tools/res_clause.ML"
-	 "Tools/res_skolem_function.ML"
-	 "Tools/res_axioms.ML"
-	 "Tools/res_types_sorts.ML"
+  "Tools/res_clause.ML"
+  "Tools/res_skolem_function.ML"
+  "Tools/res_axioms.ML"
+  "Tools/res_types_sorts.ML"
 
-	 "Tools/ATP/recon_prelim.ML"
-	 "Tools/ATP/recon_order_clauses.ML"
-	 "Tools/ATP/recon_translate_proof.ML"
-	 "Tools/ATP/recon_parse.ML"
-	 "Tools/ATP/recon_transfer_proof.ML"
-	 "Tools/ATP/VampCommunication.ML"
-	 "Tools/ATP/SpassCommunication.ML"
-	 "Tools/ATP/watcher.ML"
-	 "Tools/ATP/res_clasimpset.ML"
-	 "Tools/res_atp.ML"
-	 "Tools/reconstruction.ML"
+  "Tools/ATP/recon_prelim.ML"
+  "Tools/ATP/recon_order_clauses.ML"
+  "Tools/ATP/recon_translate_proof.ML"
+  "Tools/ATP/recon_parse.ML"
+  "Tools/ATP/recon_transfer_proof.ML"
+  "Tools/ATP/VampCommunication.ML"
+  "Tools/ATP/SpassCommunication.ML"
+  "Tools/ATP/watcher.ML"
+  "Tools/ATP/res_clasimpset.ML"
+  "Tools/res_atp.ML"
+  "Tools/reconstruction.ML"
 
 begin
 
-text{*Every theory of HOL must be a descendant or ancestor of this one!*}
-
-setup ResAxioms.clause_setup
 setup ResAxioms.meson_method_setup
 setup Reconstruction.setup