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)
```