1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  imports
     1.5    Complex_Main
     1.6    "~~/src/HOL/Library/Countable_Set"
     1.7 -  "~~/src/HOL/Library/Glbs"
     1.8    "~~/src/HOL/Library/FuncSet"
     1.9    Linear_Algebra
    1.10    Norm_Arith
    1.11 @@ -28,8 +27,6 @@
    1.12  lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
    1.13    by (rule LIMSEQ_subseq_LIMSEQ)
    1.14  
    1.15 -lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
    1.16 -
    1.17  lemma countable_PiE:
    1.18    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
    1.19    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
    1.20 @@ -1555,7 +1552,7 @@
    1.21        fix y
    1.22        assume "y \<in> {x<..} \<inter> I"
    1.23        with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
    1.24 -        by (auto intro: cInf_lower)
    1.25 +        by (auto intro!: cInf_lower bdd_belowI2)
    1.26        with a have "a < f y"
    1.27          by (blast intro: less_le_trans)
    1.28      }