# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256912579 -3600
# Node ID 47de63a883c2d6a5b4b94b8653f540e48e166371
# Parent  60acf3d3a4a0bca761d78bb84ecbc38c1a21c98e
The proper real_alpha

diff -r 60acf3d3a4a0 -r 47de63a883c2 LamEx.thy
--- a/LamEx.thy	Fri Oct 30 14:25:37 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:22:59 2009 +0100
@@ -78,7 +78,7 @@
   sorry
 
 lemma real_alpha:
-  assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
+  assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
 sorry