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)]\s)" "a\s" + assumes "t = [(a,b)]\s" "a\[b].s" shows "Lam a t = Lam b s" sorry