[isabelle-dev] NEWS: isabelle jedit options

Makarius makarius at sketis.net
Tue Jun 5 23:19:13 CEST 2018

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:

    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.


More information about the isabelle-dev mailing list