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