# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1302205670 -28800
# Node ID 445518561867e109286baa4d7b483e44e3548815
# Parent  9f44608ea28d6aff6187a168a3666b76d793be27
eqvt_lambda without eta-expansion

diff -r 9f44608ea28d -r 445518561867 Nominal/Nominal2_Base.thy
--- 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: