equal
deleted
inserted
replaced
1 (* Title: HOL/List.thy |
1 (* Title: HOL/PreList.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 2000 TU Muenchen |
4 Copyright 2000 TU Muenchen |
5 |
5 |
6 A basis for building theory List on. Is defined separately to serve as a |
6 A basis for building theory List on. Is defined separately to serve as a |
15 declare case_split [cases type: bool] |
15 declare case_split [cases type: bool] |
16 |
16 |
17 (*belongs to theory Wellfounded_Recursion*) |
17 (*belongs to theory Wellfounded_Recursion*) |
18 declare wf_induct [induct set: wf] |
18 declare wf_induct [induct set: wf] |
19 |
19 |
|
20 (*belongs to theory Datatype_Universe; hides popular names *) |
|
21 hide const Node Atom Leaf Numb Lim Funs Split Case |
|
22 |
20 end |
23 end |