On 09/04/2019 14:06, Manuel Eberl wrote: > 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.
I won't participate in this particular discussion about HOL-Algebra vs. HOL-Analysis, because I don't know much about its internal structure and applications on top of it. Just a general note for post-Isabelle2019, or post-post-Isabelle2019. The more the libraries are growing, the less it is clear how to make a hierarchy according to topics (like "Algebra", "Analysis", "Number_Theory" etc.): there will be complexities in the dependencies that might force to introduce Algebra1, Analysis1, Algebra2, Analysis2 etc. So in the worst case there is a trend towards more diverse (or amorphic?) library sessions. HOL-Analysis itself already shows such tendencies. Since some libraries are advertized as "batteries included", one could also try to organize things according to which batteries (very small to very large), e.g. AAAA Main AAA Complex_Main AA Algebra, basic Analysis C full Analysis with Homology etc. D HOL-ODE etc. For the funny letters see https://en.wikipedia.org/wiki/AAA_battery -- it merely illustrates the idea, and is not meant literally. Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
