Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Fri, 16 Apr 2010 10:47:13 +0200
changeset 1864 3d68573e46d3
parent 1863 457bf371c91a (diff)
parent 1862 310b7b768adf (current diff)
child 1865 b71b838b0a75
merged
--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 10:41:40 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 10:47:13 2010 +0200
@@ -194,6 +194,18 @@
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
+using a
+apply(induct)
+apply(perm_simp)
+apply(rule a1)
+apply(simp)
+apply(perm_simp)
+apply(rule a2)
+apply(simp)
+apply(simp)
+apply(perm_simp)
+apply(rule a3)
+apply(unfold alpha_gen)
 oops
 
 lemma
nominal2