| changeset 1561 | c3dca6e600c8 |
| parent 1553 | 4355eb3b7161 |
| child 1562 | 41294e4fc870 |
| 1560:604c4cffc5b9 | 1561:c3dca6e600c8 |
|---|---|
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = cheat_fv_rsp := false *} |
7 ML {* val _ = cheat_fv_rsp := false *} |
8 ML {* val _ = cheat_const_rsp := false *} |
8 ML {* val _ = cheat_alpha_bn_rsp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
10 |
10 |
11 nominal_datatype t = |
11 nominal_datatype t = |
12 Var "name" |
12 Var "name" |
13 | Fun "t" "t" |
13 | Fun "t" "t" |