[isabelle-dev] HOL-Algebra

[Florian Haftmann]

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", "Module". Thus the main HOL session needs to evade
via> non-standard names "Groups", "Rings", "Modules" (the latter is new
in> 2af1f142f855).

This pragmatic tradition had been started by »Orderings.thy«; I'm
uncertain whether it is worth the effort to change it.

Note that the theories »More_*.thy« contain material contributed by
Jeremy Avigad but not situated in HOL-Algebra in the first place; when
collecting this I did not want to touch the original theories, but as
part of a rework those theories could be integrated.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180517/0471e134/attachment.sig>