Tutorial/Lambda.thy
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: