As today, I would suggest omitting Ordered_Euclidean_Space and adding Complex_Transcendental. Larry
> On 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
