src/HOL/NthRoot.thy
changeset 61973 0c7e865fa7cb
parent 61969 e01015e49041
child 62131 1baed43f453e
     1.1 --- a/src/HOL/NthRoot.thy	Tue Dec 29 23:50:44 2015 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Dec 30 11:21:54 2015 +0100
     1.3 @@ -268,7 +268,7 @@
     1.4  qed (simp add: root_def[abs_def])
     1.5  
     1.6  lemma tendsto_real_root[tendsto_intros]:
     1.7 -  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
     1.8 +  "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) \<longlongrightarrow> root n x) F"
     1.9    using isCont_tendsto_compose[OF isCont_real_root, of f x F] .
    1.10  
    1.11  lemma continuous_real_root[continuous_intros]:
    1.12 @@ -457,7 +457,7 @@
    1.13  unfolding sqrt_def by (rule isCont_real_root)
    1.14  
    1.15  lemma tendsto_real_sqrt[tendsto_intros]:
    1.16 -  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
    1.17 +  "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) \<longlongrightarrow> sqrt x) F"
    1.18    unfolding sqrt_def by (rule tendsto_real_root)
    1.19  
    1.20  lemma continuous_real_sqrt[continuous_intros]: