[isabelle-dev] Homology

[Manuel Eberl]

Importing Algebra sounds like it would come with various unforeseen
consequences.

The more modular approach seems more workable to me. I for one think
that there's no rush; I'd wait until the next release cycle.

Manuel


On 09/04/2019 12: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190409/b6f5ff30/attachment-0001.html>