# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256913124 -3600
# Node ID 55b156ac4a4046df7754388d5219d26918a0b32e
# Parent  42dac1cfcd14d06d04638fafcec6b38cdd24c9ed# Parent  47de63a883c2d6a5b4b94b8653f540e48e166371
merged

diff -r 42dac1cfcd14 -r 55b156ac4a40 LamEx.thy
--- a/LamEx.thy	Fri Oct 30 15:30:33 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:32:04 2009 +0100
@@ -109,7 +109,7 @@
 sorry 
 
 lemma real_alpha:
-  assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>[b].s"
+  assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
 sorry