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/CPS3_DanvyFilinski_FCB2.thy
changeset 3197 25d11b449e92
parent 3187 b3d97424b130
child 3235 5ebd327ffb96 
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -15,8 +15,7 @@
 | "(x~)^l = l $$ (x~)"
 | "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
-  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
-  apply (rule, perm_simp, rule)
+  apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
   apply (auto simp only:)
   apply (case_tac x)
   apply (case_tac a)
nominal2