equal
deleted
inserted
replaced
1 (* Title: HOL/Induct/Tree.thy |
1 (* Title: HOL/Induct/Tree.thy |
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
2 Author: Stefan Berghofer, TU Muenchen |
4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
5 *) |
4 *) |
6 |
5 |
7 header {* Infinitely branching trees *} |
6 header {* Infinitely branching trees *} |
8 |
7 |
9 theory Tree imports Main begin |
8 theory Tree |
|
9 imports Main |
|
10 begin |
10 |
11 |
11 datatype 'a tree = |
12 datatype 'a tree = |
12 Atom 'a |
13 Atom 'a |
13 | Branch "nat => 'a tree" |
14 | Branch "nat => 'a tree" |
14 |
15 |