[isabelle-dev] Editing HOL theories interactively
bulwahn at in.tum.de
Fri Oct 12 12:28:12 CEST 2012
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
> Note that with jEdit it is now really easy to edit the HOL theories
> 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« ;-)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev