http://isabelle.in.tum.de/repos/testboard/rev/53e22c7bb5f9
Therefore I would keep Ordered_Euclidean_Space (it fits to the rest of the material in Multivariate_Analysis and is now only 300 lines).
I might be biased because I never really worked with complex numbers, but I would keep Complex_Transcendental out.
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 (I'd also vote for moving theory Complex out of Complex_Main).
Fabian On 11/4/2019 11:09 AM, Lawrence Paulson wrote:
As today, I would suggest omitting Ordered_Euclidean_Space and adding Complex_Transcendental. LarryOn 4 Nov 2019, at 15:50, Fabian Immler <[email protected]> wrote: In afp-devel/49f30bd (and its parent changesets) Tobias and I experimented with reducing the imports of many AFP-entries that build on HOL-Analysis. We introduced a theory Multivariate_Analysis to collect the theories that we deemed "Basic Analysis" material (perhaps Basic_Analysis.thy would be a better name). Currently (afp/c5c88012f116) we have 20 imports of "HOL-Analysis.Multivariate_Analysis", and 35 imports of "HOL-Analysis.Analysis", so Multivariate_Analysis seems like a reasonable point to split HOL-Analysis. The imports of Multivariate_Analysis can (or should) still be refined: It currently(isa/c85efa2be619) imports Path_Connected and Starlike and I am pretty sure much of the material in those theories is not necessary for a "Basic Analysis" library.
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
