author haftmann Sun Jul 10 22:11:32 2011 +0200 (2011-07-10) changeset 43754 09d455c93bf8 parent 43753 fe5e846c0839 child 43755 5e4a595e63fc
tuned notation
```     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}"
```