# HG changeset patch
# User nipkow
# Date 1585557310 -7200
# Node ID 2e8f861d21d428562022bec7498b0a54f09279b2
# Parent  1f957615cae6a45ecb856b012f75f733c5354707
redunant simp rule

diff -r 1f957615cae6 -r 2e8f861d21d4 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Mar 29 23:54:00 2020 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Mar 30 10:35:10 2020 +0200
@@ -420,7 +420,7 @@
     using b
     by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
   also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
-    using b by (simp add: sum.delta)
+    using b by (simp)
   also have "\<dots> = f x \<bullet> b"
     by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms)
   finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" .