Re: [isabelle] Report from our Isabelle course



> In the mean time, authors of Isabelle documentation can update their
> sources to Isabelle markdown + antiquotations as much as possible. There
> is still relatively much raw LaTeX in manuals that are not in my
> responsibility.

The Nitpick and Sledgehammer manuals are of course particular offenders in this area. The Sledgehammer manual is pretty short and should be relatively easy to port. It's on my list, but feel free to bug me again if it doesn't get done in a timely enough fashion.

As for Nitpick, the goal is to replace it with Nunchaku, so it might we better to leave the manual as is and wait until the tool is obsoleted. (Nunchaku will soon be integrated in the development Isabelle, in time for the next release, but it may take 1-2 more release cycles before Nitpick is effectively subsumed.)

As for the Nunchaku manual, I will write it in the modern style.

Jasmin





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