[isabelle-dev] Editing HOL theories interactively

Lukas Bulwahn bulwahn at in.tum.de
Fri Oct 12 12:28:12 CEST 2012

Hi Florian,

just for the record:

- I added those FIXMEs while adding the "set_comprehension_pointfree" 
- 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)


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>

More information about the isabelle-dev mailing list