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

Reply via email to