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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.