# HG changeset patch
# User wenzelm
# Date 1126732498 -7200
# Node ID a05e20f6a31a6c5b86dc491d29e6fdf437bc3873
# Parent  a8c9ed3f98186a0927e0a0ac12b68040fd27c83f
hide the rather generic names used in theory Commutative_Ring;

diff -r a8c9ed3f9818 -r a05e20f6a31a src/HOL/Main.thy
--- 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 {*