diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -3054,6 +3054,12 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
+lemma flip_fresh_fresh:
+  assumes "atom a \<sharp> x" "atom b \<sharp> x"
+  shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
+
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -3073,7 +3079,6 @@
   by (simp add: flip_commute)
 
 lemma flip_eqvt [eqvt]: 
-  fixes a b c::"'a::at_base"
   shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
   unfolding flip_def
   by (simp add: swap_eqvt atom_eqvt)
@@ -3091,6 +3096,13 @@
 text {* the following two lemmas do not hold for at_base, 
   only for single sort atoms from at *}
 
+lemma flip_triple:
+  fixes a b c::"'a::at"
+  assumes "a \<noteq> b" and "c \<noteq> b"
+  shows "(a \<leftrightarrow> c) + (b \<leftrightarrow> c) + (a \<leftrightarrow> c) = (a \<leftrightarrow> b)"
+  unfolding flip_def
+  by (rule swap_triple) (simp_all add: assms)
+
 lemma permute_flip_at:
   fixes a b c::"'a::at"
   shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
@@ -3106,14 +3118,6 @@
   and   "(a \<leftrightarrow> b) \<bullet> b = a"
   unfolding permute_flip_at by simp_all
 
-lemma flip_fresh_fresh:
-  fixes a b::"'a::at_base"
-  assumes "atom a \<sharp> x" "atom b \<sharp> x"
-  shows "(a \<leftrightarrow> b) \<bullet> x = x"
-using assms
-by (simp add: flip_def swap_fresh_fresh)
-
-
 
 subsection {* Syntax for coercing at-elements to the atom-type *}