# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271407610 -7200
# Node ID 457bf371c91a4fb9afe537b2ae65177c8cb6e2cb
# Parent  226b797868dca5a6aff1011d8ef553900ba1c902
attempt to manual prove eqvt for alpha

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