added a lemma to at_swap_simps

--- a/src/HOL/Nominal/Nominal.thy	Thu Jun 26 17:54:05 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 27 00:37:30 2008 +0200
@@ -461,6 +461,7 @@
   assumes a: "at TYPE('x)"
   shows "[(a,b)]\<bullet>a = b"
   and   "[(a,b)]\<bullet>b = a"
+  and   "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c"
   using a by (simp_all add: at_calc)
 
 lemma at4: