# HG changeset patch
# User wenzelm
# Date 1126732499 -7200
# Node ID 1ca607b286702356674577e52a115a586f57f52f
# Parent  a05e20f6a31a6c5b86dc491d29e6fdf437bc3873
imports Commutative_Ring instead of Main, since the latter hides our names;

diff -r a05e20f6a31a -r 1ca607b28670 src/HOL/ex/Commutative_Ring_Complete.thy
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 23:14:58 2005 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 23:14:59 2005 +0200
@@ -9,7 +9,7 @@
 header {* Proof of the relative completeness of method comm-ring *}
 
 theory Commutative_Ring_Complete
-imports Main
+imports Commutative_Ring  (*do not use Main here, since it hides our consts*)
 begin
 	
   (* Fromalization of normal form *)