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.thy
changeset 3192 14c7d7e29c44
parent 3187 b3d97424b130
child 3197 25d11b449e92 
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -15,6 +15,7 @@
 | "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)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (case_tac x)
   apply (case_tac a)
nominal2