Certainly it’s weird that we introduce the type of complex numbers on such a bare bones basis as to be practically useless. It is reasonable to assume that it is probably unused. But we need to deal with this appropriately to preserve compatibility.
How about this? 1: move everything currently in HOL/Complex into Complex_Analysis_Basics 2: import MacLaurin into Main, so that it now has all the other Complex_Main material: limits, transcendental functions, et cetera 3: retain the theory Complex_Main for legacy purposes, probably just for one more release. Larry > On 4 Nov 2019, at 18:41, Fabian Immler <[email protected]> wrote: > > I'd also vote for moving theory Complex out of Complex_Main). _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
