src/HOL/Lattices.thy
changeset 44919 482f1807976e
parent 44918 6a80fbc4e72c
child 44921 58eef4843641
     1.1 --- a/src/HOL/Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Sep 13 16:22:01 2011 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4    also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
     1.5      by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
     1.6    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
     1.7 -    by(simp add:inf_sup_absorb inf_commute)
     1.8 +    by(simp add: inf_commute)
     1.9    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    1.10    finally show ?thesis .
    1.11  qed
    1.12 @@ -284,7 +284,7 @@
    1.13    also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
    1.14      by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
    1.15    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    1.16 -    by(simp add:sup_inf_absorb sup_commute)
    1.17 +    by(simp add: sup_commute)
    1.18    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    1.19    finally show ?thesis .
    1.20  qed
    1.21 @@ -547,7 +547,7 @@
    1.22  
    1.23  lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
    1.24    "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
    1.25 -  by (auto simp add: less_le compl_le_compl_iff)
    1.26 +  by (auto simp add: less_le)
    1.27  
    1.28  lemma compl_less_swap1:
    1.29    assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"