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 <[email protected]> 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. > > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
