| changeset 1475 | 7f5a4cd08209 |
| parent 1396 | 48bcde67391b |
| child 1531 | e5eb247ad13c |
| 1474:3f7d67927fe2 | 1475:7f5a4cd08209 |
|---|---|
13 |
13 |
14 Univ = Arith + Sum + |
14 Univ = Arith + Sum + |
15 |
15 |
16 (** lists, trees will be sets of nodes **) |
16 (** lists, trees will be sets of nodes **) |
17 |
17 |
18 subtype (Node) |
18 typedef (Node) |
19 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" |
19 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" |
20 |
20 |
21 types |
21 types |
22 'a item = 'a node set |
22 'a item = 'a node set |
23 |
23 |