| changeset 2119 | 238062c4c9f2 |
| parent 2114 | 3201a8c3456b |
| child 2120 | 2786ff1df475 |
| 2118:0e52851acac4 | 2119:238062c4c9f2 |
|---|---|
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" |