added a lemma to at_swap_simps
authorurbanc
Fri Jun 27 00:37:30 2008 +0200 (2008-06-27)
changeset 273742a3c22fd95ab
parent 27373 5794a0e3e26c
child 27375 8d2c3d61c502
added a lemma to at_swap_simps
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Jun 26 17:54:05 2008 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Jun 27 00:37:30 2008 +0200
     1.3 @@ -461,6 +461,7 @@
     1.4    assumes a: "at TYPE('x)"
     1.5    shows "[(a,b)]\<bullet>a = b"
     1.6    and   "[(a,b)]\<bullet>b = a"
     1.7 +  and   "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c"
     1.8    using a by (simp_all add: at_calc)
     1.9  
    1.10  lemma at4: