hide many names from Datatype_Universe.
authornipkow
Fri Nov 24 16:49:27 2000 +0100 (2000-11-24)
changeset 10519ade64af4c57c
parent 10518 20d4899f5d48
child 10520 bb9dfcc87951
hide many names from Datatype_Universe.
src/HOL/Main.thy
src/HOL/PreList.thy
     1.1 --- a/src/HOL/Main.thy	Fri Nov 24 14:09:09 2000 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Nov 24 16:49:27 2000 +0100
     1.3 @@ -1,6 +1,11 @@
     1.4 +(*  Title:      HOL/Main.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2000 TU Muenchen
     1.8  
     1.9 -(*theory Main includes everything; note that theory
    1.10 -  PreList already includes most HOL theories*)
    1.11 +Theory Main includes everything.
    1.12 +Note that theory PreList already includes most HOL theories.
    1.13 +*)
    1.14  
    1.15  theory Main = Map + String:
    1.16  
     2.1 --- a/src/HOL/PreList.thy	Fri Nov 24 14:09:09 2000 +0100
     2.2 +++ b/src/HOL/PreList.thy	Fri Nov 24 16:49:27 2000 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/List.thy
     2.5 +(*  Title:      HOL/PreList.thy
     2.6      ID:         $Id$
     2.7      Author:     Tobias Nipkow
     2.8      Copyright   2000 TU Muenchen
     2.9 @@ -17,4 +17,7 @@
    2.10  (*belongs to theory Wellfounded_Recursion*)
    2.11  declare wf_induct [induct set: wf]
    2.12  
    2.13 +(*belongs to theory Datatype_Universe; hides popular names *)
    2.14 +hide const Node Atom Leaf Numb Lim Funs Split Case
    2.15 +
    2.16  end