Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LamEx.thy
changeset 245 55b156ac4a40
parent 243 22715cab3995
parent 242 47de63a883c2
child 246 6da7d538e5e0 
--- 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