diff -r b1d64b7ce2b7 -r 0532006ec7ec Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri May 07 12:28:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun May 09 11:37:19 2010 +0100
@@ -280,6 +280,11 @@
   "p \<bullet> (snd x) = snd (p \<bullet> x)"
  by (cases x) simp
 
+lemma split_eqvt[eqvt]: 
+  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+  unfolding split_def
+  by (perm_simp) (rule refl)
+
 section {* Units *}
 
 lemma supp_unit:
@@ -386,10 +391,16 @@
 
 lemma 
   fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
-  shows "(p \<bullet> (P The)) = foo"
+  shows "p \<bullet> (P The) = foo"
 apply(perm_simp exclude: The)
 oops
 
+lemma
+  fixes  P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+  shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
 thm eqvts
 thm eqvts_raw