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 > [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
