# HG changeset patch
# User paulson
# Date 1126799117 -7200
# Node ID 0382f6877b981d3201b84e126fed7ed953738a8e
# Parent  bdcffa8d8665aaf6d53ffaee7de106f6b6f0e315
moving Commutative_Ring to the correct theory

diff -r bdcffa8d8665 -r 0382f6877b98 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
 
diff -r bdcffa8d8665 -r 0382f6877b98 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Thu Sep 15 17:44:53 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Thu Sep 15 17:45:17 2005 +0200
@@ -7,7 +7,7 @@
 header{*Attributes for Reconstructing External Resolution Proofs*}
 
 theory Reconstruction
-    imports Hilbert_Choice Map Infinite_Set Extraction
+    imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
     uses "Tools/res_lib.ML"
 
 	 "Tools/res_clause.ML"