Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Fri, 30 Oct 2009 15:32:04 +0100
changeset 245 55b156ac4a40
parent 244 42dac1cfcd14 (current diff)
parent 242 47de63a883c2 (diff)
child 246 6da7d538e5e0
merged
LamEx.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2