Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real_Vector_Spaces.thy
changeset 62623 dbc62f86a1a9
parent 62533 bc25f3916a99
child 62948 7700f467892b 
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -2143,7 +2143,7 @@
     by (auto simp: lim_sequentially dist_real_def)
   { fix x :: real
     obtain n where "x \<le> real_of_nat n"
-      using ex_le_of_nat[of x] ..
+      using real_arch_simple[of x] ..
     note monoD[OF mono this]
     also have "f (real_of_nat n) \<le> y"
       by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])
isabelle