--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Jan 13 23:07:06 2016 +0100
@@ -6056,7 +6056,7 @@
apply (clarsimp simp del: divide_const_simps)
apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
done
- --\<open>Replacing @{term r} and the original (weak) premises\<close>
+ \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close>
obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
apply (rule that [of "(r + dist w z) / 2"])
apply (simp_all add: fh')