summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 22 May 2018 14:12:15 +0200 | |

changeset 68248 | ef1e0cb80fde |

parent 68246 | b48bab511939 (current diff) |

parent 68247 | 7344affc0bd4 (diff) |

child 68249 | 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 -ﬁnite 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.''