[isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

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.

Larry

> 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.