| changeset 51 | 934a58983311 |
| parent 0 | 7949f97df77a |
| 50:2e9a86203d59 | 51:934a58983311 |
|---|---|
7 |
7 |
8 Type nat is defined as a set Nat over type ind. |
8 Type nat is defined as a set Nat over type ind. |
9 *) |
9 *) |
10 |
10 |
11 Nat = WF + |
11 Nat = WF + |
12 types ind,nat 0 |
12 |
13 arities ind,nat :: term |
13 types |
14 nat :: ord |
14 ind |
15 nat |
|
16 |
|
17 arities |
|
18 ind,nat :: term |
|
19 nat :: ord |
|
15 |
20 |
16 consts |
21 consts |
17 Zero_Rep :: "ind" |
22 Zero_Rep :: "ind" |
18 Suc_Rep :: "ind => ind" |
23 Suc_Rep :: "ind => ind" |
19 Nat :: "ind set" |
24 Nat :: "ind set" |