src/HOL/Topological_Spaces.thy
changeset 54258 adfc759263ab
parent 53946 5431e1392b14
child 54797 be020ec8560c
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Nov 05 09:44:57 2013 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Nov 05 09:44:58 2013 +0100
     1.3 @@ -2112,7 +2112,7 @@
     1.4    with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
     1.5      by (auto simp: subset_eq)
     1.6    then show False
     1.7 -    using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
     1.8 +    using cInf_lower[OF `c \<in> A`] bnd by (metis not_le less_imp_le bdd_belowI)
     1.9  qed
    1.10  
    1.11  lemma Sup_notin_open:
    1.12 @@ -2125,7 +2125,7 @@
    1.13    with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
    1.14      by (auto simp: subset_eq)
    1.15    then show False
    1.16 -    using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    1.17 +    using cSup_upper[OF `c \<in> A`] bnd by (metis less_imp_le not_le bdd_aboveI)
    1.18  qed
    1.19  
    1.20  end
    1.21 @@ -2151,7 +2151,7 @@
    1.22      let ?z = "Inf (B \<inter> {x <..})"
    1.23  
    1.24      have "x \<le> ?z" "?z \<le> y"
    1.25 -      using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
    1.26 +      using `y \<in> B` `x < y` by (auto intro: cInf_lower cInf_greatest)
    1.27      with `x \<in> U` `y \<in> U` have "?z \<in> U"
    1.28        by (rule *)
    1.29      moreover have "?z \<notin> B \<inter> {x <..}"
    1.30 @@ -2163,11 +2163,11 @@
    1.31        obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
    1.32          using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
    1.33        moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    1.34 -        using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    1.35 +        using cInf_less_iff[of "B \<inter> {x <..}" "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    1.36          by (auto intro: less_imp_le)
    1.37        moreover have "?z \<le> b"
    1.38          using `b \<in> B` `x < b`
    1.39 -        by (intro cInf_lower[where z=x]) auto
    1.40 +        by (intro cInf_lower) auto
    1.41        moreover have "b \<in> U"
    1.42          using `x \<le> ?z` `?z \<le> b` `b < min a y`
    1.43          by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)