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 <[email protected]> > > 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).
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
