[isabelle-dev] NEWS: isabelle jedit options

Lawrence Paulson lp15 at cam.ac.uk
Wed Jun 6 12:45:39 CEST 2018

I saw them of course, but what do they do?

> On 5 Jun 2018, at 22:19, Makarius <makarius at sketis.net> wrote:
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>>> On 5 Jun 2018, at 22:01, Makarius <makarius at sketis.net> wrote:
>>> These options are very relevant for the coming release. I am interested
>>> to get feedback from early adopters, if this is already sufficient or
>>> requires further refinement.
> The NEWS contains these examples:
>  Examples:
>    isabelle jedit -R HOL-Number_Theory
>    isabelle jedit -R HOL-Number_Theory -A HOL
>    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
>    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
> Here are more examples:
>    isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
>    isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
>    isabelle jedit -d '$AFP' -S Deep_Learning
> Alexander Bentkamp needs to be credited for writing a clear
> specification of the intermediate image Deep_Learning_Lib: {* Theories
> that are not part of HOL-Probability but are used by this entry *}.
> From there it was reasonably easy to implement the above options, but
> users need to start using them, and stop publishing old development
> artefacts in AFP.
> 	Makarius

More information about the isabelle-dev mailing list