removed Commutative_Ring hacks;
authorwenzelm
Tue Sep 20 14:03:38 2005 +0200 (2005-09-20)
changeset 17509054cd8972095
parent 17508 c84af7f39a6b
child 17510 5e3ce025e1a5
removed Commutative_Ring hacks;
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Tue Sep 20 14:03:37 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Sep 20 14:03:38 2005 +0200
     1.3 @@ -14,16 +14,6 @@
     1.4  
     1.5  subsection {* Special hacks, late package setup etc. *}
     1.6  
     1.7 -text {* \medskip Hide the rather generic names used in theory @{text
     1.8 -  Commutative_Ring}. *}
     1.9 -
    1.10 -hide (open) const
    1.11 -  Pc Pinj PX
    1.12 -  Pol Add Sub Mul Pow Neg
    1.13 -  add mul neg sqr pow sub
    1.14 -  norm
    1.15 -
    1.16 -
    1.17  text {* \medskip Default values for rufute, see also theory @{text
    1.18    Refute}.
    1.19  *}