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/CPS1_Plotkin.thy
changeset 3191 0440bc1a2438
parent 3187 b3d97424b130
child 3192 14c7d7e29c44 
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -30,7 +30,6 @@
 apply simp
 thm Abs1_eq_iff
 apply(subst Abs1_eq_iff)
-apply(auto)[2]
 apply(rule disjI2)
 apply(rule conjI)
 apply(simp)
@@ -130,11 +129,10 @@
 apply (rename_tac M N u K)
 apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) =  Lam u (M+ $$ u~ $$ K)")
 apply (simp only:)
-apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
+apply (auto simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base)[1]
 apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))")
 apply (simp only:)
-apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
-apply(simp_all add: flip_def[symmetric])
+apply (simp add: Abs1_eq_iff flip_fresh_fresh fresh_at_base)
 apply (case_tac "m = ma")
 apply simp_all
 apply (case_tac "m = na")
nominal2