<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    On 04/16/2012 09:13 AM, Christian Sternagel wrote:
    <blockquote cite="mid:4F8BC6A4.2050501@jaist.ac.jp" type="cite">Hi
      all,
      <br>
      <br>
      On 04/03/2012 02:51 AM, Florian Haftmann wrote:
      <br>
      <blockquote type="cite">well, I suggest to augment the existing
        theory with lemmas transferred
        <br>
        from relpow to relpowp to emphasize that both worlds exists and
        that
        <br>
        lemmas can be found easier by find_theorems.  The typical
        pattern is
        <br>
        <br>
        lemma foo_relpow: …
        <br>
           <proof>
        <br>
        <br>
        lemma foo_relpowp: …
        <br>
           by (fact foo_relpow [to_pred])
        <br>
        <br>
      </blockquote>
      I did this in the meantime (tested with "isabelle makeall all").
      This time as a patch (in order to avoid cluttering the history) on
      Theory Transitive_Closure. Suggested NEWS entry:
      <br>
      <br>
      ------------------------------------------------------------------
      <br>
      * Theory Transitive_Closure: Duplicated facts about "relpow" for
      "relpowp" to emphasize that both worlds exist and facilitate
      better results with "find_theorems".
      <br>
      <br>
        Added Lemmas:
      <br>
        relpowp_1
      <br>
        relpowp_0_I
      <br>
        relpowp_Suc_I
      <br>
        relpowp_Suc_I2
      <br>
        relpowp_0_E
      <br>
        relpowp_Suc_E
      <br>
        relpowp_E
      <br>
        relpowp_Suc_D2
      <br>
        relpowp_Suc_E2
      <br>
        relpowp_Suc_D2'
      <br>
        relpowp_E2
      <br>
        relpowp_add
      <br>
        relpowp_commute
      <br>
        relpowp_bot
      <br>
        rtranclp_imp_Sup_relpowp
      <br>
        relpowp_imp_rtranclp
      <br>
        rtranclp_is_Sup_relpowp
      <br>
        rtranclp_power
      <br>
        tranclp_power
      <br>
        rtranclp_imp_relpowp
      <br>
        relpowp_fun_conv
      <br>
      ------------------------------------------------------------------
      <br>
      <br>
    </blockquote>
    I pushed your changes to the public repository, but I did not
    consider the NEWS entry worth mentioning -- we add theorems on a
    daily basis, without explicitly advertising them in the NEWS.<br>
    <br>
    Lukas <br>
    <blockquote cite="mid:4F8BC6A4.2050501@jaist.ac.jp" type="cite">cheers
      <br>
      <br>
      chris
      <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>