src/HOL/PreList.thy
changeset 10733 59f82484e000
parent 10680 26e4aecf3207
child 11787 85b3735a51e1
     1.1 --- a/src/HOL/PreList.thy	Sat Dec 23 22:50:19 2000 +0100
     1.2 +++ b/src/HOL/PreList.thy	Sat Dec 23 22:50:39 2000 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/PreList.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 +    Author:     Tobias Nipkow and Markus Wenzel
     1.8      Copyright   2000 TU Muenchen
     1.9  
    1.10  A basis for building theory List on. Is defined separately to serve as a
    1.11 @@ -19,6 +19,7 @@
    1.12  
    1.13  (*belongs to theory Datatype_Universe; hides popular names *)
    1.14  hide const Node Atom Leaf Numb Lim Funs Split Case
    1.15 +hide type node item
    1.16  
    1.17  
    1.18  (* generic summation indexed over nat *)