[isabelle-dev] NEWS: isabelle jedit options

Lawrence Paulson lp15 at cam.ac.uk
Wed Jun 6 18:13:57 CEST 2018

I just tried

	isabelle jedit -R HOL-UNITY

assuming that it would build an auxiliary image for HOL-Auth, which is imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so things are pretty subtle here. A little more explanation would be valuable.


> On 6 Jun 2018, at 16:36, Makarius <makarius at sketis.net> wrote:
> It could just mean that these examples don't need an auxiliary image.
> Take the first example from NEWS:
>  isabelle jedit -R HOL-Number_Theory
> It produces an image
> "HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also
> the title line of Isabelle/jEdit.
> It also puts you into the ROOT entry for HOL-Number_Theory, so you can
> directly explore its theories in the Prover IDE.

More information about the isabelle-dev mailing list