# HG changeset patch
# User nipkow
# Date 1526991123 -7200
# Node ID 7344affc0bd429dadba83c8b156b90c08fb7f00c
# Parent  37974ddde92844c3389aab7e2977b350f737568a
removed unicode symbol

diff -r 37974ddde928 -r 7344affc0bd4 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue May 22 11:05:47 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue May 22 14:12:03 2018 +0200
@@ -287,7 +287,7 @@
 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
-finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
+finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
 the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
 can integrate all derivatives.''