src/HOL/Main.thy

--- a/src/HOL/Main.thy	Thu Sep 15 17:44:53 2005 +0200
+++ b/src/HOL/Main.thy	Thu Sep 15 17:45:17 2005 +0200
@@ -6,7 +6,8 @@
 header {* Main HOL *}
 
 theory Main
-imports Commutative_Ring Refute Reconstruction
+imports Refute Reconstruction 
+        (*other theores need to be ancestors of Reconstruction, not Main!!*)
 
 begin