author | wenzelm |
Tue, 22 Nov 2005 19:37:36 +0100 | |
changeset 18230 | 4dc1f30af6a1 |
parent 18229 | e5a624483a23 |
child 18231 | 2eea98bbf650 |
--- a/src/HOL/Datatype.thy Tue Nov 22 19:34:50 2005 +0100 +++ b/src/HOL/Datatype.thy Tue Nov 22 19:37:36 2005 +0100 @@ -79,8 +79,8 @@ subsection {* Finishing the datatype package setup *} text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} -hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr -hide type node item +hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr +hide (open) type node item subsection {* Further cases/induct rules for tuples *}