| changeset 14274 | 0cb8a9a144d2 |
| parent 14208 | 144f45277d5a |
| child 14981 | e73f8140af78 |
--- a/src/HOL/Datatype.thy Thu Dec 04 16:16:36 2003 +0100 +++ b/src/HOL/Datatype.thy Thu Dec 04 21:57:15 2003 +0100 @@ -78,7 +78,7 @@ subsection {* Finishing the datatype package setup *} text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} -hide const Node Atom Leaf Numb Lim Split Case Suml Sumr +hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr hide type node item