<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">I would try to avoid HOL-Algebra as much as
possible. The entire library is not in a great state and
introducing unnecessary dependencies on it should be avoided.</font></p>
<p><font size="+1">There is much work to be done there.</font></p>
<p><font size="+1">Manuel</font></p>
<div class="moz-cite-prefix">On 09/04/2019 15:25, Makarius wrote:<br>
</div>
<blockquote type="cite"
cite="mid:ccfeec12-6eb6-2439-0625-84a145e91efd@sketis.net">
<pre class="moz-quote-pre" wrap="">On 09/04/2019 14:06, Manuel Eberl wrote:
</pre>
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">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.
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">
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 <a class="moz-txt-link-freetext" href="https://en.wikipedia.org/wiki/AAA_battery">https://en.wikipedia.org/wiki/AAA_battery</a> --
it merely illustrates the idea, and is not meant literally.
Makarius
</pre>
</blockquote>
</body>
</html>