author | wenzelm |
Tue, 20 Sep 2005 14:03:38 +0200 | |
changeset 17509 | 054cd8972095 |
parent 17508 | c84af7f39a6b |
child 17510 | 5e3ce025e1a5 |
src/HOL/Main.thy | file | annotate | diff | comparison | revisions |
--- 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}. *}