I saw them of course, but what do they do? Larry > On 5 Jun 2018, at 22:19, Makarius <makar...@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 <makar...@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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev