diff -r e13e70f32407 -r e01015e49041 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 29 22:41:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 29 23:04:53 2015 +0100
@@ -1957,7 +1957,7 @@
       qed
     qed
   qed
-  then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) ----> g x" ..
+  then obtain g where g: "\<forall>x\<in>s. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
   have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
   proof (rule, rule)
     fix e :: real