Re: [isabelle] Facelifting Isabelle tutorial

On 18/02/2016 15:09, Serguei Mokhov wrote:
Hello all,

Are there plans to facelift a bit the tutorial document in Isabelle
distribution? Is anyone working on it slowly?

No. It is largely subsumed by the other tutorials. Hence "Programming and Proving in Isabelle/HOL" says that the proof style is outdated. Maybe the web page should move the tutorial down the list.


If not, are contributions to it welcome or is it not worth the effort?
In particular, at the very least:

- While there is a good volume of good stuff in there for instance it
still refers to Proof General in its tooltips; these could be
"refactored" into the way it is now done in jEdit with new tips added
or obsolete non-replaceable removed.
- prog-prove and other docs have appeared over the last few years with
some more recent info, so at least these can be all referenced in the
beginning in the introduction to direct the reader to those other
places based on their need on datatypes, functions, locales, etc..
This is such that the tutorial cold be the starting point for all
branching out to other documentation, while the rest is being updated
or just stays as-is self-contained.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.