--- 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" .