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 -
```