--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Dec 29 23:50:44 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Dec 30 11:21:54 2015 +0100
@@ -2881,8 +2881,8 @@
qed
lemma tendsto_infnorm [tendsto_intros]:
- assumes "(f ---> a) F"
- shows "((\<lambda>x. infnorm (f x)) ---> infnorm a) F"
+ assumes "(f \<longlongrightarrow> a) F"
+ shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
proof (rule tendsto_compose [OF LIM_I assms])
fix r :: real
assume "r > 0"