changeset 2116 | ce228f7b2b72 |
parent 2105 | e25b0fff0dd2 |
child 2120 | 2786ff1df475 |
2115:9b109ef7bf47 | 2116:ce228f7b2b72 |
---|---|
5 (* example 8 from Peter Sewell's bestiary *) |
5 (* example 8 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = cheat_fv_rsp := true *} |
9 ML {* val _ = cheat_fv_rsp := true *} |
10 ML {* val _ = cheat_equivp := true *} |
|
10 ML {* val _ = cheat_alpha_bn_rsp := true *} |
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
11 |
12 |
12 nominal_datatype exp = |
13 nominal_datatype exp = |
13 EVar name |
14 EVar name |
14 | EUnit |
15 | EUnit |