Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
changeset 3191 0440bc1a2438
parent 3187 b3d97424b130
child 3192 14c7d7e29c44 
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -27,8 +27,7 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
   apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
-  apply(simp)
+  apply (simp add: flip_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order
@@ -52,7 +51,7 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
   apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
+  apply (simp add: flip_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order
nominal2