diff -r 5ebd327ffb96 -r e2da10806a34 Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Mon May 19 12:45:26 2014 +0100 +++ b/Tutorial/Lambda.thy Mon May 19 16:45:46 2014 +0100 @@ -47,7 +47,7 @@ apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order @@ -76,7 +76,7 @@ apply(simp add: perm_supp_eq fresh_star_Pair) done -termination (eqvt) +nominal_termination (eqvt) by lexicographic_order lemma fresh_fact: