# HG changeset patch
# User wenzelm
# Date 1127217818 -7200
# Node ID 054cd897209521d03ada145d4f84da5524ed5734
# Parent  c84af7f39a6bbcdde659e45ef1cd5a960acdcb9d
removed Commutative_Ring hacks;

diff -r c84af7f39a6b -r 054cd8972095 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Sep 20 14:03:37 2005 +0200
+++ b/src/HOL/Main.thy	Tue Sep 20 14:03:38 2005 +0200
@@ -14,16 +14,6 @@
 
 subsection {* Special hacks, late package setup etc. *}
 
-text {* \medskip 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
-
-
 text {* \medskip Default values for rufute, see also theory @{text
   Refute}.
 *}