<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">Importing Algebra sounds like it would come with
various unforeseen consequences.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">Manuel</font></p>
<p><font size="+1"></font><br>
</p>
<div class="moz-cite-prefix">On 09/04/2019 12:14, Lawrence Paulson
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:BA381B8B-AF1F-4002-9E9E-80C4A30D7489@cam.ac.uk">
<pre class="moz-quote-pre" wrap="">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
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>