# HG changeset patch
# User wenzelm
# Date 1159645162 -7200
# Node ID 46694b230cfb8ca6c537ce321c8f2bd8e4a7764a
# Parent  3275b03e2fffb57e0a3fbca2b047774353d71bba
hides popular names (from Datatype.thy);

diff -r 3275b03e2fff -r 46694b230cfb src/HOL/Datatype_Universe.thy
--- a/src/HOL/Datatype_Universe.thy	Sat Sep 30 21:39:20 2006 +0200
+++ b/src/HOL/Datatype_Universe.thy	Sat Sep 30 21:39:22 2006 +0200
@@ -533,6 +533,13 @@
 lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
 by auto
 
+
+subsection {* Finishing the datatype package setup *}
+
+text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
+hide (open) const Push Node Atom Leaf Numb Lim Split Case
+hide (open) type node item
+
 ML
 {*
 val apfst_conv = thm "apfst_conv";