[isabelle-dev] Reorganising Analysis

[Lawrence Paulson]

As today, I would suggest omitting Ordered_Euclidean_Space and adding Complex_Transcendental.
Larry

> On 4 Nov 2019, at 15:50, Fabian Immler <immler at in.tum.de> 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.