# HG changeset patch
# User huffman
# Date 1235075823 28800
# Node ID c09f348ca88a36c00d35554eb1de5fe86f635756
# Parent  62efbd0ef132b04ffd23f48f4c71e3f71829df7b
declare xor_compl_{left,right} [simp]

diff -r 62efbd0ef132 -r c09f348ca88a src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Thu Feb 19 12:26:32 2009 -0800
+++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Feb 19 12:37:03 2009 -0800
@@ -223,7 +223,7 @@
 lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
 by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
 
-lemma xor_compl_left: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
+lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
 apply (simp only: conj_disj_distribs)
 apply (simp only: conj_cancel_right conj_cancel_left)
@@ -231,7 +231,7 @@
 apply (simp only: disj_ac conj_ac)
 done
 
-lemma xor_compl_right: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
+lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
 apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
 apply (simp only: conj_disj_distribs)
 apply (simp only: conj_cancel_right conj_cancel_left)
@@ -239,11 +239,11 @@
 apply (simp only: disj_ac conj_ac)
 done
 
-lemma xor_cancel_right [simp]: "x \<oplus> \<sim> x = \<one>"
+lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>"
 by (simp only: xor_compl_right xor_self compl_zero)
 
-lemma xor_cancel_left [simp]: "\<sim> x \<oplus> x = \<one>"
-by (subst xor_commute) (rule xor_cancel_right)
+lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>"
+by (simp only: xor_compl_left xor_self compl_zero)
 
 lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
 proof -