| changeset 1595 | aeed597d2043 |
| parent 1576 | 7b8f570b2450 |
| 1594:892fcdb96c96 | 1595:aeed597d2043 |
|---|---|
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
|
8 ML {* val _ = cheat_equivp := false *} |
|
9 |
7 |
10 nominal_datatype kind = |
8 nominal_datatype kind = |
11 Type |
9 Type |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
10 | KPi "ty" n::"name" k::"kind" bind n in k |
13 and ty = |
11 and ty = |