equal
deleted
inserted
replaced
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_fv_rsp = ref false *} |
|
9 ML {* val cheat_const_rsp = ref false *} |
|
10 ML {* val cheat_equivp = ref false *} |
|
11 ML {* val cheat_fv_eqvt = ref false *} |
|
12 ML {* val cheat_alpha_eqvt = ref false *} |
7 |
13 |
8 nominal_datatype kind = |
14 nominal_datatype kind = |
9 Type |
15 Type |
10 | KPi "ty" n::"name" k::"kind" bind n in k |
16 | KPi "ty" n::"name" k::"kind" bind n in k |
11 and ty = |
17 and ty = |