1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:56:39 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:11:32 2011 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    "\<Squnion>{a, b} = a \<squnion> b"
     1.5    by (simp add: Sup_empty Sup_insert)
     1.6  
     1.7 -lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     1.8 +lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     1.9    by (auto intro: Inf_greatest dest: Inf_lower)
    1.10  
    1.11  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    1.12 @@ -227,12 +227,12 @@
    1.13  lemma Inf_less_iff:
    1.14    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.15    shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    1.16 -  unfolding not_le[symmetric] le_Inf_iff by auto
    1.17 +  unfolding not_le [symmetric] le_Inf_iff by auto
    1.18  
    1.19  lemma less_Sup_iff:
    1.20    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.21    shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    1.22 -  unfolding not_le[symmetric] Sup_le_iff by auto
    1.23 +  unfolding not_le [symmetric] Sup_le_iff by auto
    1.24  
    1.25  lemma INF_less_iff:
    1.26    fixes a :: "'a::{complete_lattice,linorder}"