# HG changeset patch
# User nipkow
# Date 975080967 -3600
# Node ID ade64af4c57c6a14eacef5643cd8bee374d0e180
# Parent  20d4899f5d481707855d2f76274772e66ed99036
hide many names from Datatype_Universe.

diff -r 20d4899f5d48 -r ade64af4c57c src/HOL/Main.thy
--- 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:
 
diff -r 20d4899f5d48 -r ade64af4c57c src/HOL/PreList.thy
--- 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