1.1 --- a/src/HOL/Complete_Lattice.thy Sun Jul 10 22:11:32 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Sun Jul 10 22:17:33 2011 +0200
1.3 @@ -362,10 +362,10 @@
1.4 qed
1.5
1.6 lemma Inter_subset:
1.7 - "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
1.8 + "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
1.9 by (fact Inf_less_eq)
1.10
1.11 -lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
1.12 +lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
1.13 by (fact Inf_greatest)
1.14
1.15 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"