diff -r a70b89a3e02e -r 0c7e865fa7cb src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Dec 29 23:50:44 2015 +0100
+++ b/src/HOL/Complex.thy	Wed Dec 30 11:21:54 2015 +0100
@@ -382,14 +382,14 @@
 lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
 
 lemma tendsto_Complex [tendsto_intros]:
-  "(f ---> a) F \<Longrightarrow> (g ---> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
+  "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
   by (auto intro!: tendsto_intros)
 
 lemma tendsto_complex_iff:
-  "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
+  "(f \<longlongrightarrow> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F \<and> ((\<lambda>x. Im (f x)) \<longlongrightarrow> Im x) F)"
 proof safe
-  assume "((\<lambda>x. Re (f x)) ---> Re x) F" "((\<lambda>x. Im (f x)) ---> Im x) F"
-  from tendsto_Complex[OF this] show "(f ---> x) F"
+  assume "((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F" "((\<lambda>x. Im (f x)) \<longlongrightarrow> Im x) F"
+  from tendsto_Complex[OF this] show "(f \<longlongrightarrow> x) F"
     unfolding complex.collapse .
 qed (auto intro: tendsto_intros)
 
@@ -530,7 +530,7 @@
 lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
 lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
 
-lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
+lemma lim_cnj: "((\<lambda>x. cnj(f x)) \<longlongrightarrow> cnj l) F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
   by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)
 
 lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"