removed Commutative_Ring hacks;
authorwenzelm
Tue, 20 Sep 2005 14:03:38 +0200
changeset 17509 054cd8972095
parent 17508 c84af7f39a6b
child 17510 5e3ce025e1a5
removed Commutative_Ring hacks;
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}.
 *}