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/Multivariate_Analysis/Weierstrass.thy
changeset 62623 dbc62f86a1a9
parent 61945 1135b8de26c3
child 62843 313d3b697c9a 
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -725,7 +725,7 @@
   { fix e::real
     assume e: "0 < e"
     then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
-      by (auto simp: real_arch_inv [of e])
+      by (auto simp: real_arch_inverse [of e])
     { fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real"
       assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
       assume x: "x \<in> s"
isabelle