Re: [isabelle] Proof_Context abstraction
On Wed, 30 Jul 2014, Lars Hupel wrote:
And for code in my own modules Ctrl-Hover is very helpful, but that
doesn’t work in ML files that have been loaded in the heap. Is there
maybe a way to get jEdit process Pure (instead of loading a Heap)?
As far as I know, that is only possible for theories loaded *after* Pure
has been bootstrapped. You're probably out of luck there.
That is why I have moved more and more tools within Pure into Pure.thy
itself, so that they can be loaded into another theory as well, for
inspecting within the Prover IDE.
This archive was generated by a fusion of
Pipermail (Mailman edition) and