diff -r 000327cea3eb -r b9718519f3d2 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy Tue Aug 21 20:52:18 2007 +0200
+++ b/src/HOL/Library/Boolean_Algebra.thy Tue Aug 21 20:53:37 2007 +0200
@@ -81,7 +81,7 @@
subsection {* Conjunction *}
-lemma conj_absorb: "x \ x = x"
+lemma conj_absorb [simp]: "x \ x = x"
proof -
have "x \ x = (x \ x) \ \" using disj_zero_right by simp
also have "... = (x \ x) \ (x \ \ x)" using conj_cancel_right by simp
@@ -94,7 +94,7 @@
lemma conj_zero_right [simp]: "x \ \ = \"
proof -
have "x \ \ = x \ (x \ \ x)" using conj_cancel_right by simp
- also have "... = (x \ x) \ \ x" using conj_assoc by simp
+ also have "... = (x \ x) \ \ x" using conj_assoc by (simp only:)
also have "... = x \ \ x" using conj_absorb by simp
also have "... = \" using conj_cancel_right by simp
finally show ?thesis .