# HG changeset patch
# User wenzelm
# Date 1456685817 -3600
# Node ID 11e06f5283bc441589a730b053ebc0d4fb20c8cf
# Parent  2026ef279d1ecd4d0f7b6562f4f0af49e8e35a7f
proper document source;

diff -r 2026ef279d1e -r 11e06f5283bc src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- 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