# HG changeset patch
# User haftmann
# Date 1310328692 -7200
# Node ID 09d455c93bf8798628d270bcec563ef6fb7394f6
# Parent  fe5e846c0839f323e05996d4e434a4de2fcaba97
tuned notation

diff -r fe5e846c0839 -r 09d455c93bf8 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:56:39 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:11:32 2011 +0200
@@ -82,7 +82,7 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_empty Sup_insert)
 
-lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
 
 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
@@ -227,12 +227,12 @@
 lemma Inf_less_iff:
   fixes a :: "'a\<Colon>{complete_lattice,linorder}"
   shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
-  unfolding not_le[symmetric] le_Inf_iff by auto
+  unfolding not_le [symmetric] le_Inf_iff by auto
 
 lemma less_Sup_iff:
   fixes a :: "'a\<Colon>{complete_lattice,linorder}"
   shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
-  unfolding not_le[symmetric] Sup_le_iff by auto
+  unfolding not_le [symmetric] Sup_le_iff by auto
 
 lemma INF_less_iff:
   fixes a :: "'a::{complete_lattice,linorder}"