| changeset 1360 | c54cb3f7ac70 |
| parent 1348 | 2e2a3cd58f64 |
| child 1429 | 866208388c1d |
| 1359:3bf496a971c6 | 1360:c54cb3f7ac70 |
|---|---|
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 = |