# HG changeset patch # User wenzelm # Date 977608239 -3600 # Node ID 59f82484e00058870eaaa67f9bc89b6612eb6c20 # Parent d4fda7d05ce51c948acec28408ae3637a5796d04 hide type node item; diff -r d4fda7d05ce5 -r 59f82484e000 src/HOL/PreList.thy --- a/src/HOL/PreList.thy Sat Dec 23 22:50:19 2000 +0100 +++ b/src/HOL/PreList.thy Sat Dec 23 22:50:39 2000 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/PreList.thy ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow and Markus Wenzel Copyright 2000 TU Muenchen A basis for building theory List on. Is defined separately to serve as a @@ -19,6 +19,7 @@ (*belongs to theory Datatype_Universe; hides popular names *) hide const Node Atom Leaf Numb Lim Funs Split Case +hide type node item (* generic summation indexed over nat *)