Datatype_Universe: hide base names only;
authorwenzelm
Tue Nov 22 19:37:36 2005 +0100 (2005-11-22)
changeset 182304dc1f30af6a1
parent 18229 e5a624483a23
child 18231 2eea98bbf650
Datatype_Universe: hide base names only;
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Nov 22 19:34:50 2005 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Nov 22 19:37:36 2005 +0100
     1.3 @@ -79,8 +79,8 @@
     1.4  subsection {* Finishing the datatype package setup *}
     1.5  
     1.6  text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
     1.7 -hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
     1.8 -hide type node item
     1.9 +hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    1.10 +hide (open) type node item
    1.11  
    1.12  
    1.13  subsection {* Further cases/induct rules for tuples *}