changeset 2986 | 847972b7b5ba |
parent 2984 | 1b39ba5db2c1 |
child 2998 | f0fab367453a |
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Fri Aug 12 22:37:41 2011 +0200 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Sun Aug 14 08:52:03 2011 +0200 @@ -217,7 +217,7 @@ apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) done -termination +termination (eqvt) by lexicographic_order definition psi:: "lt => lt"