[isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring
hoelzl at in.tum.de
Mon Mar 30 11:37:39 CEST 2015
Merged & pushed with 5fd0b3c8a355.
Am Montag, den 30.03.2015, 06:39 +0000 schrieb 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
> there have been no problems.
> Isabelle: db0b87085c16
> AFP: 55e04ff27c52
> >> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev