[isabelle-dev] Reorganising Analysis
immler at in.tum.de
Mon Nov 4 19:41:56 CET 2019
I just checked: it is easy to remove Path_Connected and Starlike from
the imports of Ordered_Euclidean_Space:
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).
On 11/4/2019 11:09 AM, Lawrence Paulson wrote:
> As today, I would suggest omitting Ordered_Euclidean_Space and adding Complex_Transcendental.
>> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev