# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271407633 -7200
# Node ID 3d68573e46d37f493297c9f31a404097e34046f1
# Parent  457bf371c91a4fb9afe537b2ae65177c8cb6e2cb# Parent  310b7b768adfd394d765ec96d57458cbc5c6d0b4
merged

diff -r 310b7b768adf -r 3d68573e46d3 Nominal/Ex/Lambda.thy
--- 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