# HG changeset patch # User nipkow # Date 1526991135 -7200 # Node ID ef1e0cb80fde5d67f1dd90b34ff292a6336d188a # Parent b48bab5119391a03af2288617d063b809d35d3e2# Parent 7344affc0bd429dadba83c8b156b90c08fb7f00c merged diff -r b48bab511939 -r ef1e0cb80fde src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- 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.''