[isabelle-dev] Reorganising Analysis

[Lawrence Paulson]

Then the obvious stopping point is one line above: Derivative.

The problem at the moment with basing a development around the Cauchy integral theorem is that you might also  want to include Winding_Numbers, but that theory inherits almost the whole of Analysis: even the Jordan curve theorem.

Larry

> On 4 Nov 2019, at 12:19, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> Great work, thanks for taking care of this!
> 
> Just abstractly speaking, it would seem very odd to me to have a "complex analysis" directory without integration. Complex integration and the Cauchy integral formula are such basic tools in complex analysis that not including them in a "complex analysis" entry would seem… unusual to me.
> 
> Perhaps "complex analysis prerequisites".
>