src/HOL/Real_Vector_Spaces.thy
 changeset 53381 355a4cac5440 parent 53374 a14d2a854c02 child 53600 8fda7ad57466
```     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
1.3 @@ -833,7 +833,8 @@
1.4    show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
1.5    proof (rule ext, safe)
1.6      fix S :: "real set" assume "open S"
1.7 -    then guess f unfolding open_real_def bchoice_iff ..
1.8 +    then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
1.9 +      unfolding open_real_def bchoice_iff ..
1.10      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
1.11        by (fastforce simp: dist_real_def)
1.12      show "generate_topology (range lessThan \<union> range greaterThan) S"
1.13 @@ -1525,7 +1526,8 @@
1.14    with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
1.15      by (auto simp: LIMSEQ_def dist_real_def)
1.16    { fix x :: real
1.17 -    from ex_le_of_nat[of x] guess n ..
1.18 +    obtain n where "x \<le> real_of_nat n"
1.19 +      using ex_le_of_nat[of x] ..
1.20      note monoD[OF mono this]
1.21      also have "f (real_of_nat n) \<le> y"
1.22        by (rule LIMSEQ_le_const[OF limseq])
```