hide the rather generic names used in theory Commutative_Ring;

--- a/src/HOL/Main.thy	Wed Sep 14 23:14:57 2005 +0200
+++ b/src/HOL/Main.thy	Wed Sep 14 23:14:58 2005 +0200
@@ -15,6 +15,18 @@
   PreList} already includes most HOL theories.
 *}
 
+
+subsection {* Misc *}
+
+text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *}
+
+hide (open) const
+  Pc Pinj PX
+  Pol Add Sub Mul Pow Neg
+  add mul neg sqr pow sub
+  norm
+
+
 subsection {* Configuration of the code generator *}
 
 types_code
@@ -70,6 +82,7 @@
 
 lemmas [code] = imp_conv_disj
 
+
 subsection {* Configuration of the 'refute' command *}
 
 text {*