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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
