No problem. I will take care of the split. Wenda
> On 5 Nov 2019, at 12:55, Tobias Nipkow <[email protected]> wrote: > > I stumbled across this oddity - the important concept of winding numbers > being defined in the middle of Cauchy_Integral_Theorem - myself this morning > just looking at the toc. Thus I am all in favour of splitting off Winding > Numbers from Cauchy_Integral_Theorem: the latter contains 1000 lines of > material following the definition up to subsection "Cauchy's integral > formula, again for a convex enclosing set". Later there is some more material: > subsection ‹More winding number properties› > > Wenda, would you mind performing this split that you suggested? > Not sure about the names: Maybe Winding_Numbers and Winding_Numbers_Applied? > Any better ideas? > > Tobias > > On 05/11/2019 01:54, Wenda Li wrote: >>> On 4 Nov 2019, at 12:48, Manuel Eberl <[email protected] >>> <mailto:[email protected]>> wrote: >>> >>> I don't really have an idea of what material you really need for winding >>> numbers. I recall that Wenda had some problems with them (about what >>> happens when there's a pole on the path) – perhaps it would make sense to >>> give that theory an overhaul altogether? >> Our definition of winding numbers is fine to me, as it follows classic >> analytical textbook definition which usually does not allow the target point >> on the path. Unless we want to further generalise the definition in a >> topological or algebraic direction (which does not seem too necessary at the >> moment), this point-on-the-path issue is probably what we have to live with. >> My two cents about our winding numbers is the organisation: winding numbers >> are (kind of secretly) defined in Cauchy_Integral_Theorem.th >> <http://cauchy_integral_theorem.th>y rather than in Winding_Numbers.thy >> <https://isabelle.in.tum.de/repos/isabelle/file/c85efa2be619/src/HOL/Analysis/Winding_Numbers.thy>, >> which only contains advanced facts related to winding numbers. Maybe it is >> worth having two theories about winding numbers — a basic one for the >> integral theorem and an advanced one that is on the top of Jordan_Curve & >> Riemann_Mapping. >> Wenda >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
