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.
Nominal/Nominal2_Base.thy
changeset 2753 445518561867
parent 2743 7085ab735de7
child 2760 8f833ebc4b58 
--- 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