
diff -r 226b797868dc -r 457bf371c91a Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 10:18:16 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 10:46:50 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




