[isabelle-dev] NEWS: isabelle jedit options

[Makarius]

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