[isabelle-dev] Complex.thy

[Lawrence Paulson]

The motivation for moving Complex.thy was simply that Complex_Transcendental and Complex_Analysis_Basics are now adjacent and could even be combined. All this material could conceivably reside in a single theory.

As for Analysis itself: it is simply too big but where to divide it is somewhat arbitrary. One option is to take Derivative and everything above it. There is something natural about having a development with a lot about topology, limits, norms and derivatives but nothing about integration. It would also have nothing about the complex numbers except the tiny Complex.thy, which is perhaps another reason to move it.

Larry

> On 20 Nov 2019, at 16:36, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> On the other hand, I'm not sure what your exact plans for restructuring are, but I thought we were going to have some session that contains complex number and the basic operations on them but not integration. Then Computational_Algebra could import that. Or perhaps Complex could import Computational_Algebra (not sure if that makes sense). But as I said, I also don't see a problem with simply moving those few theorems out of Formal_Power_Series.
> 
>