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.
eqvt_lambda without eta-expansion
authorChristian Urban <urbanc@in.tum.de>
Fri, 08 Apr 2011 03:47:50 +0800
changeset 2753 445518561867
parent 2752 9f44608ea28d
child 2754 2a3a37f29f4f
eqvt_lambda without eta-expansion
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Base.thy	Wed Apr 06 13:47:08 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Apr 08 03:47:50 2011 +0800
@@ -733,7 +733,7 @@
 
 lemma eqvt_lambda:
   fixes f :: "'a::pt \<Rightarrow> 'b::pt"
-  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+  shows "p \<bullet> f \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
   unfolding permute_fun_def unpermute_def by simp
 
 lemma eqvt_bound:
nominal2