merged
authornipkow
Tue, 22 May 2018 14:12:15 +0200
changeset 68249 ef1e0cb80fde
parent 68247 b48bab511939 (current diff)
parent 68248 7344affc0bd4 (diff)
child 68250 949d93804740
merged
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri May 18 17:51:58 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue May 22 14:12:15 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.''