diff -r 8f51702e1f2e -r 52730e5ec8cb Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Wed May 23 23:57:27 2012 +0100 +++ b/Nominal/Nominal2_Base.thy Thu May 24 10:17:32 2012 +0200 @@ -1093,6 +1093,9 @@ unfolding finite_def by (perm_simp) (rule refl) +lemma Let_eqvt [eqvt]: + "p \ Let x y = Let (p \ x) (p \ y)" + unfolding Let_def permute_fun_app_eq .. subsubsection {* Equivariance for product operations *}