equal
deleted
inserted
replaced
7 |
7 |
8 theory Tree |
8 theory Tree |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 datatype 'a tree = |
12 datatype_new 'a tree = |
13 Atom 'a |
13 Atom 'a |
14 | Branch "nat => 'a tree" |
14 | Branch "nat => 'a tree" |
15 |
15 |
16 primrec map_tree :: "('a => 'b) => 'a tree => 'b tree" |
16 primrec map_tree :: "('a => 'b) => 'a tree => 'b tree" |
17 where |
17 where |
32 by (induct ts) auto |
32 by (induct ts) auto |
33 |
33 |
34 |
34 |
35 subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*} |
35 subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*} |
36 |
36 |
37 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" |
37 datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" |
38 |
38 |
39 text{*Addition of ordinals*} |
39 text{*Addition of ordinals*} |
40 primrec add :: "[brouwer,brouwer] => brouwer" |
40 primrec add :: "[brouwer,brouwer] => brouwer" |
41 where |
41 where |
42 "add i Zero = i" |
42 "add i Zero = i" |