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