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/Foo2.thy
changeset 2594 515e5496171c
parent 2593 25dcb2b1329e
child 2598 b136721eedb2 
--- a/Nominal/Ex/Foo2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -43,17 +43,6 @@
 thm foo.supp
 thm foo.fresh
 
-lemma uu1:
-  shows "alpha_bn as (permute_bn p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[5]
-apply(simp only: foo.perm_bn_simps)
-apply(simp only: foo.eq_iff)
-apply(simp only: foo.perm_bn_simps)
-apply(simp only: foo.eq_iff refl)
-apply(simp)
-done
-
 lemma tt1:
   shows "(p \<bullet> bn as) = bn (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
@@ -286,10 +275,10 @@
 apply(rule conjI)
 apply(assumption)
 apply(rule conjI)
-apply(rule uu1)
+apply(rule foo.perm_bn_alpha)
 apply(rule conjI)
 apply(assumption)
-apply(rule uu1)
+apply(rule foo.perm_bn_alpha)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
@@ -348,7 +337,6 @@
 apply(erule exE)+
 apply(rule assms(2))
 apply(assumption)
-apply(erule exE)+
 apply(rule assms(3))
 apply(auto)[2]
 apply(erule exE)+
nominal2