hide Push
authornipkow
Thu Dec 04 21:57:15 2003 +0100 (2003-12-04)
changeset 142740cb8a9a144d2
parent 14273 e33ffff0123c
child 14275 031a5a051bb4
hide Push
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Thu Dec 04 16:16:36 2003 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Thu Dec 04 21:57:15 2003 +0100
     1.3 @@ -78,7 +78,7 @@
     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 Node Atom Leaf Numb Lim Split Case Suml Sumr
     1.8 +hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
     1.9  hide type node item
    1.10  
    1.11