[isabelle-dev] Fwd: Re: [isabelle] Formalizing Gaussian integers in Isabelle
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...
More information about the isabelle-dev