[isabelle-dev] Reorganising Analysis

Lawrence Paulson lp15 at cam.ac.uk
Mon Nov 4 13:44:04 CET 2019

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.


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

More information about the isabelle-dev mailing list