| changeset 1576 | 7b8f570b2450 |
| parent 1561 | c3dca6e600c8 |
| child 1595 | aeed597d2043 |
| 1575:2c37f5a8c747 | 1576:7b8f570b2450 |
|---|---|
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 {* val _ = cheat_fv_rsp := false *} |
|
9 ML {* val _ = cheat_alpha_bn_rsp := false *} |
|
10 ML {* val _ = cheat_equivp := false *} |
8 ML {* val _ = cheat_equivp := false *} |
11 |
9 |
12 nominal_datatype kind = |
10 nominal_datatype kind = |
13 Type |
11 Type |
14 | KPi "ty" n::"name" k::"kind" bind n in k |
12 | KPi "ty" n::"name" k::"kind" bind n in k |