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/Limits.thy
changeset 65204 d23eded35a33
parent 65036 ab7e11730ad8
child 65578 e4997c181cce 
--- a/src/HOL/Limits.thy	Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Limits.thy	Fri Mar 10 23:16:40 2017 +0100
@@ -729,7 +729,7 @@
     by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
 qed
 
-lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
+lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]
 
 
 subsubsection \<open>Linear operators and multiplication\<close>
isabelle