[isabelle-dev] HOL-Algebra

Lawrence Paulson lp15 at cam.ac.uk
Sat May 12 11:40:58 CEST 2018

I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are ancient. They desperately need updating and streamlining.

We’ve decided that Group-Ring-Module is irremediable, and are using it only as a list of useful results that need to be done again.


> On 11 May 2018, at 23:40, Makarius <makarius at sketis.net> wrote:
> Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to
> my information, Clemens Ballarin has taken great care about HOL-Algebra
> over many years (even with contributions by students).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180512/e2c25c03/attachment-0002.html>

More information about the isabelle-dev mailing list