# HG changeset patch
# User paulson
# Date 1102432570 -3600
# Node ID e56ce5cefe9cde7898d3cc54ef5c9f22f75d27e6
# Parent  780ea4c697f2a7918051820e663076c85929b076
all theories must be related to Reconstruction

diff -r 780ea4c697f2 -r e56ce5cefe9c src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Dec 07 16:15:44 2004 +0100
+++ b/src/HOL/Main.thy	Tue Dec 07 16:16:10 2004 +0100
@@ -6,7 +6,7 @@
 header {* Main HOL *}
 
 theory Main
-    imports Map Infinite_Set Extraction Refute Reconstruction
+    imports Extraction Refute Reconstruction
 
 begin
 
diff -r 780ea4c697f2 -r e56ce5cefe9c src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Tue Dec 07 16:15:44 2004 +0100
+++ b/src/HOL/Reconstruction.thy	Tue Dec 07 16:16:10 2004 +0100
@@ -7,7 +7,7 @@
 header{*Attributes for Reconstructing External Resolution Proofs*}
 
 theory Reconstruction
-    imports Hilbert_Choice
+    imports Hilbert_Choice Map Infinite_Set
     files "Tools/res_lib.ML"
 	  "Tools/res_clause.ML"
 	  "Tools/res_skolem_function.ML"
@@ -18,6 +18,8 @@
 
 begin
 
+text{*Every theory of HOL must be a descendant or ancestor of this one!*}
+
 setup Reconstruction.setup
 
 end
\ No newline at end of file