--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon May 19 16:45:46 2014 +0100
@@ -63,7 +63,7 @@
apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
@@ -89,7 +89,7 @@
apply (simp add: Abs1_eq_iff CPS.eqvt)
by blast
-termination (eqvt)
+nominal_termination (eqvt)
by (relation "measure size") (simp_all)
lemma convert_supp[simp]:
@@ -143,7 +143,7 @@
apply(simp_all add: flip_fresh_fresh)
done
-termination (eqvt)
+nominal_termination (eqvt)
by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
section{* lemma related to Kapply *}