On 06/06/18 16:19, Lawrence Paulson wrote:
> According to the NEWS entry, option -R builds an auxiliary logic image. I 
> tried this with a couple of examples and no images were built. According to 
> the manual, this option opens the ROOT entry. It does seem to do that, though 
> I'm not sure why this facility is needed.

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.

isabelle-dev mailing list

Reply via email to