nipkow at in.tum.de
Tue Apr 9 13:28:43 CEST 2019
I would second this suggestion not to rearrange analysis before the release.
There are mnay users of Analysis but there will only be a few Homology users.
On 09/04/2019 12:49, Dr A. Koutsoukou-Argyraki wrote:
> why not leave it as a separate Homology library that would be importing both
> Analysis and Algebra for now?
> It would then evolve into an Algebraic Topology library with time.
> This would also reflect how a "real-life" math library would be organised.
> i.e. : I would prefer your suggestion of breaking up Analysis into several
> modules some of which may need to port Homology (and thus Algebra too)
> and some not (if I correctly understand what you mean).
> Could this be done at a second stage in time for Isabelle 2020 ?
> Would that be feasible?
> On 2019-04-09 11:14, Lawrence Paulson wrote:
>> I’ve completed porting HOL Light’s homology library, which many people
>> have requested, and I’m trying to install it now into Analysis. This
>> will have one big consequence: Analysis will now import Algebra. This
>> in turn affects all theories that depend on Analysis.
>> An alternative may be to break up Analysis into several modules,
>> though I don’t see how that can be done in time for the next release.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev