<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hi Florian,<br>
    <br>
    just for the record:<br>
    <br>
    - I added those FIXMEs while adding the
    "set_comprehension_pointfree" simproc.<br>
    - If this FIXME would have been a trivial exercise, I would have
    done it immediately. However, moving is only possible after some
    further changes in the simproc itself.<br>
    - In the meantime, I did find time to address the issues (cf.
    bed063d0c526, 9979d64b8016 and b28dbb7a45d9)<br>
    <br>
    Lukas<br>
    <br>
    <br>
    On 10/06/2012 04:12 PM, Florian Haftmann wrote:
    <blockquote cite="mid:50703C5B.4060100@informatik.tu-muenchen.de"
      type="cite">
      <pre wrap="">Hi all,

I stumbled over some comments »(* FIXME: move to Set theory *)« in
Finite_Set.thy.

Note that with jEdit it is now really easy to edit the HOL theories
interactively:

        isabelle build -b Pure && isabelle jedit -l Pure <thy files>

So, you can get your intention done directly and need not to imitate the
school book pattern »This is left as an exercise to the reader« ;-)

Cheers,
        Florian

</pre>
      <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>
    <br>
  </body>
</html>