changeset 10519 | ade64af4c57c |
parent 10261 | bb2f1e859177 |
child 10671 | ac6b3b671198 |
--- 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