--- a/src/HOL/NthRoot.thy Tue Dec 29 23:50:44 2015 +0100
+++ b/src/HOL/NthRoot.thy Wed Dec 30 11:21:54 2015 +0100
@@ -268,7 +268,7 @@
qed (simp add: root_def[abs_def])
lemma tendsto_real_root[tendsto_intros]:
- "(f ---> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
+ "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) \<longlongrightarrow> root n x) F"
using isCont_tendsto_compose[OF isCont_real_root, of f x F] .
lemma continuous_real_root[continuous_intros]:
@@ -457,7 +457,7 @@
unfolding sqrt_def by (rule isCont_real_root)
lemma tendsto_real_sqrt[tendsto_intros]:
- "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
+ "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) \<longlongrightarrow> sqrt x) F"
unfolding sqrt_def by (rule tendsto_real_root)
lemma continuous_real_sqrt[continuous_intros]: