diff -r 4239a0784e5f -r 2fe45593aaa9 Quot/Nominal/Nominal2_Base.thy
--- a/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 16:05:59 2010 +0100
+++ b/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 20:02:44 2010 +0100
@@ -433,6 +433,17 @@
 unfolding permute_fun_def permute_bool_def
 unfolding vimage_def Collect_def mem_def ..
 
+lemma swap_set_not_in:
+  assumes a: "a \<notin> S" "b \<notin> S"
+  shows "(a \<rightleftharpoons> b) \<bullet> S = S"
+  using a by (auto simp add: permute_set_eq swap_atom)
+
+lemma swap_set_in:
+  assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
+  shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
+  using a by (auto simp add: permute_set_eq swap_atom)
+
+
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -954,8 +965,7 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
-
-section {* support and freshness for applications *}
+section {* Support and freshness for applications *}
 
 lemma supp_fun_app:
   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"