<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div class="BodyFragment"><font size="2"><span style="font-size:10pt;">
<div class="PlainText">Dear all,<br>
<br>
can someone please integrate the attached patch which introduces a locale for semirings.<br>
<br>
I tested the patch by running all sessions of the AFP though without ISABELLE_FULL_TEST:<br>
there have been no problems.<br>
<br>
Isabelle: db0b87085c16<br>
AFP:      55e04ff27c52<br>
<br>
Thanks,<br>
René<br>
<br>
</div>
</span></font></div>
<div class="BodyFragment"><font size="2"><span style="font-size:10pt;">
<div class="PlainText"><br>
<br>
> <br>
>> Looks like a good idea to me. Are there any drawbacks?<br>
> <br>
> None of which I'm aware of. I just tested my changes against three AFP-entries which are based on HOL-Algebra
<br>
> and they all compile without problems. (Jordan_Hoelder Secondary_Sylow VectorSpace)<br>
> <br>
> However, I really just adapted Ring.thy by adding semiring as intermediate locale. I did not make further
<br>
> changes at this point, e.g., by also having commutative semirings, homomorphisms on semirings, etc.<br>
<br>
</div>
</span></font></div>
</body>
</html>