equal
deleted
inserted
replaced
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* The binding structure is too complicated, so equivalence the |
9 (* The binding structure is too complicated, so equivalence the |
10 way we define it is not true *) |
10 way we define it is not true *) |
11 ML {* val _ = cheat_equivp := true *} |
|
12 |
11 |
13 ML {* val _ = recursive := false *} |
12 ML {* val _ = recursive := false *} |
14 nominal_datatype exp6 = |
13 nominal_datatype exp6 = |
15 EVar name |
14 EVar name |
16 | EPair exp6 exp6 |
15 | EPair exp6 exp6 |