--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Feb 28 19:54:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Feb 28 19:56:57 2016 +0100
@@ -200,7 +200,7 @@
text \<open>
John Harrison writes as follows:
-``The usual assumption in complex analysis texts is that a path \<gamma> should be piecewise
+``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise
continuously differentiable, which ensures that the path integral exists at least for any continuous
f, since all piecewise continuous functions are integrable. However, our notion of validity is
weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a