[isabelle-dev] Editing HOL theories interactively

[Lukas Bulwahn]

Hi Florian,

just for the record:

- I added those FIXMEs while adding the "set_comprehension_pointfree" 
simproc.
- 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.
- In the meantime, I did find time to address the issues (cf. 
bed063d0c526, 9979d64b8016 and b28dbb7a45d9)

Lukas


On 10/06/2012 04:12 PM, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121012/92e30485/attachment-0002.html>