[isabelle-dev] Fwd: Re: [isabelle] Formalizing Gaussian integers in Isabelle

[Lawrence Paulson]

We do have a new formalisation of abstract algebra, due to Clemens:

 https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html

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?

Larry
---------- Forwarded message ----------
Date: 17 Jan 2020, 09:03 +0000
To: Manuel Eberl <eberlm at in.tum.de>

>
> Sorry about this – HOL-Algebra is not used very much and is /really/ messy.
>
> I think I'll have a shot at cleaning up the type classes enough to be
> usable in your case during the next few weeks. I can't say yet if it
> will work out though, but hopefully this will be done by the next
> release (which I guess will be some time around April or May).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200117/6d5f4fef/attachment.html>