| changeset 2114 | 3201a8c3456b |
| parent 2105 | e25b0fff0dd2 |
| child 2116 | ce228f7b2b72 |
| 2113:af11e9fbc45a | 2114:3201a8c3456b |
|---|---|
10 *) |
10 *) |
11 |
11 |
12 atom_decl name |
12 atom_decl name |
13 atom_decl coname |
13 atom_decl coname |
14 |
14 |
15 ML {* val _ = cheat_alpha_eqvt := true *} |
|
16 ML {* val _ = cheat_equivp := true *} |
15 ML {* val _ = cheat_equivp := true *} |
17 ML {* val _ = cheat_fv_rsp := true *} |
16 ML {* val _ = cheat_fv_rsp := true *} |
18 |
17 |
19 nominal_datatype trm = |
18 nominal_datatype trm = |
20 Ax "name" "coname" |
19 Ax "name" "coname" |