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.
Description: S/MIME Cryptographic Signature