--- 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
--- 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"