tuned notation
authorhaftmann
Sun Jul 10 22:17:33 2011 +0200 (2011-07-10)
changeset 437555e4a595e63fc
parent 43754 09d455c93bf8
child 43756 15ea1a07a8cf
tuned notation
src/HOL/Complete_Lattice.thy
     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}"