On 04/11/2019 19:41, Fabian Immler wrote: > I might be biased because I never really worked with complex numbers, > but I would keep Complex_Transcendental out.
I have been working with complex numbers a lot and think they are the best thing ever, but I don't object. If a clean separation can be made, I don't see why we shouldn't make it there. The downside would be that e.g. the Gamma function would not be available in this "reduced" Analysis image. > This is simply because I find it easier to draw the line before complex > numbers instead of having to argue which parts of complex analysis should be > part of this "Basic Analysis" session and which ones should not The obvious choice would be: all the complex analogues of standard real operations (exp, ln, sin, cos, tan) and the most basic operations (cis, Arg). Possibly the Gamma function. But nothing that involves integration. (Gamma_Function contains a few things using integrals, but I think those can easily be pulled out) > I'd also vote for moving theory Complex out of Complex_Main That probably makes a lot of sense in any case. Manuel _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
