src/HOL/Library/Boolean_Algebra.thy
changeset 24393 b9718519f3d2
parent 24357 d42cf77da51f
child 25283 c532fd8445a2
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Tue Aug 21 20:52:18 2007 +0200
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Tue Aug 21 20:53:37 2007 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  subsection {* Conjunction *}
     1.6  
     1.7 -lemma conj_absorb: "x \<sqinter> x = x"
     1.8 +lemma conj_absorb [simp]: "x \<sqinter> x = x"
     1.9  proof -
    1.10    have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" using disj_zero_right by simp
    1.11    also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
    1.12 @@ -94,7 +94,7 @@
    1.13  lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
    1.14  proof -
    1.15    have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
    1.16 -  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by simp
    1.17 +  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by (simp only:)
    1.18    also have "... = x \<sqinter> \<sim> x" using conj_absorb by simp
    1.19    also have "... = \<zero>" using conj_cancel_right by simp
    1.20    finally show ?thesis .