Hi all,
just a few comments on my behalf.
>> 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.
Seems to make sense.
> Just one oddity in HOL-Algebra: It claims canonical theory names like>
> "Group", "Ring",
Hi Makarius,
> I have studied this a bit further. The interval
> 75130777ece4:d45b78cb86cf contains more than just the string type
> change, but it is still the main thing. Here are also other sessions in
> similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498:
>
> * faster:
