src/HOL/Main.thy
changeset 17509 054cd8972095
parent 17461 83f1dd9d901d
child 17601 a6a322f96145
     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  *}