[isabelle-dev] Homology

[Tobias Nipkow]

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.

Tobias

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?
> 
> Best,
> Angeliki
> 
> 
> 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.
>>
>> Larry
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190409/38c84129/attachment-0001.bin>