<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html;
      charset=windows-1252">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Great, thanks!<br>
    <br>
    Alexander<br>
    <br>
    <br>
    <div class="moz-cite-prefix">Am 06.10.2018 um 13:06 schrieb Tobias
      Nipkow:<br>
    </div>
    <blockquote type="cite"
      cite="mid:8c1bf18e-1289-911d-8403-c17e8a828576@in.tum.de">Since
      Alexander cannot push changes, I have done so now.
      <br>
      <br>
      Tobias
      <br>
      <br>
      On 28/09/2018 18:44, Lawrence Paulson wrote:
      <br>
      <blockquote type="cite">Sounds good to me!
        <br>
        Larry
        <br>
        <br>
        <blockquote type="cite">On 28 Sep 2018, at 14:00, Alexander
          Maletzky <<a class="moz-txt-link-abbreviated" href="mailto:alexander.maletzky@risc.jku.at">alexander.maletzky@risc.jku.at</a>
          <a class="moz-txt-link-rfc2396E" href="mailto:alexander.maletzky@risc.jku.at"><mailto:alexander.maletzky@risc.jku.at></a>> wrote:
          <br>
          <br>
          <br>
          lemma "sum_image_le" in theory "Groups_Big", which is stated
          for
          <br>
          type-class "ordered_ab_group_add", holds more generally for
          <br>
          "ordered_comm_monoid_add" (proof below). May I propose to
          change it
          <br>
          accordingly?
          <br>
          <br>
          Best regards,
          <br>
          Alexander
          <br>
        </blockquote>
        <br>
        <br>
        <br>
        _______________________________________________
        <br>
        isabelle-dev mailing list
        <br>
        <a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
        <br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
        <br>
        <br>
      </blockquote>
      <br>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>