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