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
