<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>