--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jul 20 23:59:09 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Jul 24 16:50:46 2017 +0100
@@ -5305,8 +5305,7 @@
}
then show lintg: "l contour_integrable_on \<gamma>"
apply (simp add: contour_integrable_on)
- apply (blast intro: integrable_uniform_limit_real)
- done
+ by (metis (mono_tags, lifting)integrable_uniform_limit_real)
{ fix e::real
define B' where "B' = B + 1"
have B': "B' > 0" "B' > B" using \<open>0 \<le> B\<close> by (auto simp: B'_def)