| changeset 2114 | 3201a8c3456b |
| parent 2105 | e25b0fff0dd2 |
| child 2120 | 2786ff1df475 |
| 2113:af11e9fbc45a | 2114:3201a8c3456b |
|---|---|
4 |
4 |
5 (* example 3 from Peter Sewell's bestiary *) |
5 (* example 3 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = cheat_alpha_eqvt := true *} |
|
10 ML {* val _ = cheat_equivp := true *} |
9 ML {* val _ = cheat_equivp := true *} |
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
10 ML {* val _ = cheat_alpha_bn_rsp := true *} |
12 |
11 |
13 nominal_datatype exp = |
12 nominal_datatype exp = |
14 Var "name" |
13 Var "name" |