diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -398,7 +398,7 @@
   by transfer (auto simp: algebra_simps setsum_subtractf)
 
 lemma norm_blinfun_of_matrix:
-  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
+  "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
   apply (rule norm_blinfun_bound)
    apply (simp add: setsum_nonneg)
   apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
@@ -413,7 +413,7 @@
 proof -
   have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
-  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
+  hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
     by (auto intro!: Zfun_setsum)
   thus ?thesis
     unfolding tendsto_Zfun_iff blinfun_of_matrix_minus