changeset 1655 | 9cec4269b7f9 |
parent 1604 | 5ab97f43ec24 |
child 1656 | c9d3dda79fe3 |
--- a/Nominal/ExPS6.thy Fri Mar 26 10:35:26 2010 +0100 +++ b/Nominal/ExPS6.thy Fri Mar 26 10:55:13 2010 +0100 @@ -6,7 +6,8 @@ atom_decl name -(* The binding structure is too complicated, so we cannot show equivalence *) +(* The binding structure is too complicated, so equivalence the + way we define it is not true *) ML {* val _ = cheat_equivp := true *} ML {* val _ = recursive := false *}