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