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

[Johannes Hölzl]

Merged & pushed with 5fd0b3c8a355.

  - Johannes

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
> 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.
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev