| changeset 1364 | 226693549aa0 |
| parent 1360 | c54cb3f7ac70 |
| child 1429 | 866208388c1d |
| 1363:f00761b5957e | 1364:226693549aa0 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 ML {* restricted_nominal := false *} |
8 ML {* restricted_nominal := 2 *} |
9 |
9 |
10 nominal_datatype kind = |
10 nominal_datatype kind = |
11 Type |
11 Type |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
13 and ty = |
13 and ty = |