--- a/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 22:04:23 2013 +0200
@@ -833,7 +833,8 @@
show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
proof (rule ext, safe)
fix S :: "real set" assume "open S"
- then guess f unfolding open_real_def bchoice_iff ..
+ then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
+ unfolding open_real_def bchoice_iff ..
then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
by (fastforce simp: dist_real_def)
show "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1525,7 +1526,8 @@
with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
by (auto simp: LIMSEQ_def dist_real_def)
{ fix x :: real
- from ex_le_of_nat[of x] guess n ..
+ obtain n where "x \<le> real_of_nat n"
+ using ex_le_of_nat[of x] ..
note monoD[OF mono this]
also have "f (real_of_nat n) \<le> y"
by (rule LIMSEQ_le_const[OF limseq])