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

author | wenzelm |

Sun, 28 Feb 2016 19:56:57 +0100 | |

changeset 62456 | 11e06f5283bc |

parent 62455 | 2026ef279d1e |

child 62458 | 9590972c2caf |

child 62459 | 7a5d88dd8cc9 |

proper document source;

src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy | file | annotate | diff | comparison | revisions |

--- 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