hide many names from Datatype_Universe.

--- a/src/HOL/Main.thy	Fri Nov 24 14:09:09 2000 +0100
+++ b/src/HOL/Main.thy	Fri Nov 24 16:49:27 2000 +0100
@@ -1,6 +1,11 @@
+(*  Title:      HOL/Main.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2000 TU Muenchen
 
-(*theory Main includes everything; note that theory
-  PreList already includes most HOL theories*)
+Theory Main includes everything.
+Note that theory PreList already includes most HOL theories.
+*)
 
 theory Main = Map + String:
 

--- a/src/HOL/PreList.thy	Fri Nov 24 14:09:09 2000 +0100
+++ b/src/HOL/PreList.thy	Fri Nov 24 16:49:27 2000 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/List.thy
+(*  Title:      HOL/PreList.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TU Muenchen
@@ -17,4 +17,7 @@
 (*belongs to theory Wellfounded_Recursion*)
 declare wf_induct [induct set: wf]
 
+(*belongs to theory Datatype_Universe; hides popular names *)
+hide const Node Atom Leaf Numb Lim Funs Split Case
+
 end