diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/Beta.thy --- a/Nominal/Ex/Beta.thy Mon May 19 12:45:26 2014 +0100 +++ b/Nominal/Ex/Beta.thy Mon May 19 16:45:46 2014 +0100 @@ -34,7 +34,7 @@ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma forget: