[isabelle-dev] Reorganising Analysis

Manuel Eberl eberlm at in.tum.de
Mon Nov 4 13:19:30 CET 2019

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


On 04/11/2019 12:55, Lawrence Paulson wrote:
> With a little help from Fabian, I managed to prove the inverse
> function theorem and therefore to reduce somewhat the theories
> involved in building Complex_Transcendental, which can now be combined
> with Complex_Analysis_Basics. There are still 25 ancestor theories.
> Arguably this material should be moved to its own directory,
> Complex_Analysis. This development would include quite a bit of basic
> topology but no integration or measure theory.
> If we do this as the first step, the next step should become clearer.
> I already think it might be based on integration. Any thoughts or
> reactions?
> Larry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/93ba9c8d/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screenshot 2019-11-04 at 11.25.42.png
Type: image/png
Size: 600354 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/93ba9c8d/attachment-0001.png>

More information about the isabelle-dev mailing list