[isabelle-dev] NEWS: isabelle jedit options
lp15 at cam.ac.uk
Wed Jun 6 18:13:57 CEST 2018
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 <makarius at 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.
More information about the isabelle-dev