changeset 3236 | e2da10806a34 |
parent 3235 | 5ebd327ffb96 |
--- 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: