[isabelle-dev] Homology

[Dr A. Koutsoukou-Argyraki]

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