
<html xmlns="http://www.w3.org/1999/xhtml">

<head>

<title></title>

</head>

<body>

<div name="messageBodySection">

<div dir="auto">We do have a new formalisation of abstract algebra, due to Clemens:

<div dir="auto"><br /></div>

<div dir="auto"> <a href="https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html">https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html</a></div>

<div dir="auto"><br /></div>

<div dir="auto">It doesn’t go very far. But it seems far superior to our existing library. How can we develop this further while preserving its elegance?</div>

</div>

</div>

<div name="messageSignatureSection"><br />

<div class="matchFont">

<div dir="auto">Larry</div>

</div>

</div>

<div name="messageReplySection">---------- Forwarded message ----------<br />

<b>Date:</b> 17 Jan 2020, 09:03 +0000<br />

<b>To:</b> Manuel Eberl <eberlm@in.tum.de><br />

<br />

<blockquote type="cite" class="spark_quote" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;"><br />

<div>Sorry about this – HOL-Algebra is not used very much and is /really/ messy.<br />

<br />

I think I'll have a shot at cleaning up the type classes enough to be<br />

usable in your case during the next few weeks. I can't say yet if it<br />

will work out though, but hopefully this will be done by the next<br />

release (which I guess will be some time around April or May).</div>

</blockquote>

</div>

</body>

</html>