# HG changeset patch
# User urbanc
# Date 1214519850 -7200
# Node ID 2a3c22fd95ab72544fca7adaed66961c3753b59a
# Parent  5794a0e3e26ce8b49793e45c15675894fe299272
added a lemma to at_swap_simps

diff -r 5794a0e3e26c -r 2a3c22fd95ab src/HOL/Nominal/Nominal.thy
--- 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: