# HG changeset patch
# User haftmann
# Date 1310329053 -7200
# Node ID 5e4a595e63fc6f4febe2584ffa0b67e5b9bfb8ea
# Parent  09d455c93bf8798628d270bcec563ef6fb7394f6
tuned notation

diff -r 09d455c93bf8 -r 5e4a595e63fc src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:11:32 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:17:33 2011 +0200
@@ -362,10 +362,10 @@
 qed
 
 lemma Inter_subset:
-  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
+  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_less_eq)
 
-lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
+lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
   by (fact Inf_greatest)
 
 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"