equal
deleted
inserted
replaced
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_const_rsp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
9 ML {* val _ = cheat_equivp := false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
|
11 ML {* val _ = cheat_alpha_eqvt := false *} |
|
12 |
10 |
13 nominal_datatype t = |
11 nominal_datatype t = |
14 Var "name" |
12 Var "name" |
15 | Fun "t" "t" |
13 | Fun "t" "t" |
16 and tyS = |
14 and tyS = |