Nominal/ExPS6.thy
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  *}