src/HOL/Analysis/Bounded_Linear_Function.thy

--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -548,7 +548,7 @@
     fix e::real
     let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
     assume "e > 0"
-    hence "e / ?d > 0" by (simp add: DIM_positive)
+    hence "e / ?d > 0" by (simp)
     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
       by simp
     moreover