# HG changeset patch
# User huffman
# Date 1187722417 -7200
# Node ID b9718519f3d227394a2b2f261440d5b821d8293f
# Parent  000327cea3eb2fd581b9dd3e73c0caea96777688
declare conj_absorb [simp]

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 \<sqinter> x = x"
+lemma conj_absorb [simp]: "x \<sqinter> x = x"
 proof -
   have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" using disj_zero_right by simp
   also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
@@ -94,7 +94,7 @@
 lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
 proof -
   have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
-  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by simp
+  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by (simp only:)
   also have "... = x \<sqinter> \<sim> x" using conj_absorb by simp
   also have "... = \<zero>" using conj_cancel_right by simp
   finally show ?thesis .