# HG changeset patch
# User wenzelm
# Date 1390664713 -3600
# Node ID fb10f6ce0c1638f112ef8cec96853d33e999bf71
# Parent  bc8cf4312ea7143c6bd0b4032dd5c2c63700adc4
tuned proof;

diff -r bc8cf4312ea7 -r fb10f6ce0c16 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jan 25 16:35:15 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jan 25 16:45:13 2014 +0100
@@ -1514,8 +1514,7 @@
     assume i: "i \<in> Basis"
     have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
       norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
-      by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf uminus_add_conv_diff
-            norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
+      by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
     also have "\<dots> \<le> e + e"
       unfolding real_norm_def
       by (intro add_mono norm_bound_Basis_le i fPs) auto