changeset 2984 | 1b39ba5db2c1 |
parent 2965 | d8a6b424f80a |
child 2998 | f0fab367453a |
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Fri Jul 22 11:52:12 2011 +0100 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Sun Jul 24 07:54:54 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"