src/HOL/Library/Boolean_Algebra.thy
changeset 29996 c09f348ca88a
parent 29629 5111ce425e7a
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Thu Feb 19 12:26:32 2009 -0800
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Feb 19 12:37:03 2009 -0800
     1.3 @@ -223,7 +223,7 @@
     1.4  lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
     1.5  by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
     1.6  
     1.7 -lemma xor_compl_left: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
     1.8 +lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
     1.9  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
    1.10  apply (simp only: conj_disj_distribs)
    1.11  apply (simp only: conj_cancel_right conj_cancel_left)
    1.12 @@ -231,7 +231,7 @@
    1.13  apply (simp only: disj_ac conj_ac)
    1.14  done
    1.15  
    1.16 -lemma xor_compl_right: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
    1.17 +lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
    1.18  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
    1.19  apply (simp only: conj_disj_distribs)
    1.20  apply (simp only: conj_cancel_right conj_cancel_left)
    1.21 @@ -239,11 +239,11 @@
    1.22  apply (simp only: disj_ac conj_ac)
    1.23  done
    1.24  
    1.25 -lemma xor_cancel_right [simp]: "x \<oplus> \<sim> x = \<one>"
    1.26 +lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>"
    1.27  by (simp only: xor_compl_right xor_self compl_zero)
    1.28  
    1.29 -lemma xor_cancel_left [simp]: "\<sim> x \<oplus> x = \<one>"
    1.30 -by (subst xor_commute) (rule xor_cancel_right)
    1.31 +lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>"
    1.32 +by (simp only: xor_compl_left xor_self compl_zero)
    1.33  
    1.34  lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
    1.35  proof -