[isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring

[Thiemann, Rene]

Dear all,

can someone please integrate the attached patch which introduces a locale for semirings.

I tested the patch by running all sessions of the AFP though without ISABELLE_FULL_TEST:
there have been no problems.

Isabelle: db0b87085c16
AFP:      55e04ff27c52

Thanks,
René



>
>> Looks like a good idea to me. Are there any drawbacks?
>
> None of which I'm aware of. I just tested my changes against three AFP-entries which are based on HOL-Algebra
> and they all compile without problems. (Jordan_Hoelder Secondary_Sylow VectorSpace)
>
> However, I really just adapted Ring.thy by adding semiring as intermediate locale. I did not make further
> changes at this point, e.g., by also having commutative semirings, homomorphisms on semirings, etc.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150330/4070119f/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: semiring.patch
Type: application/octet-stream
Size: 5322 bytes
Desc: semiring.patch
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150330/4070119f/attachment.obj>