[isabelle-dev] Reorganising Analysis

[Manuel Eberl]

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

Manuel


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>