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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
