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

Lawrence Paulson lp15 at cam.ac.uk
Fri Jan 17 11:43:25 CET 2020

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


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?

---------- 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>

More information about the isabelle-dev mailing list