[isabelle-dev] Reorganising Analysis
nipkow at in.tum.de
Mon Nov 4 21:00:56 CET 2019
I am very much in agreement here.
On 04/11/2019 19:41, Fabian Immler wrote:
> 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
>>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev