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