[isabelle-dev] Isabelle Programming Tutorial

[Christian Urban]

This is NOT an April Fools' Joke ;o)

Hi,

almost a year ago we started a project to lower the entry
barrier for users to program on the ML-level of Isabelle.
We now have a draft for the Isabelle Programming Tutorial.
See

  http://isabelle.in.tum.de/nominal/activities/idp/

As usual with such documents, they are always incomplete
and work in progress. However, a few people already found
the current draft quite useful. A big thanks to Stefan
Berghofer, Sacha Böhme, Jeremy Dawson, Alexander Krauss,
Armin Heller and Christian Sternagel, who contributed to
the tutorial.

The tutorial is aimed at students to become familiar with
the Isabelle code as quickly as possible. To improve the
tutorial further and close the gaps, WE NEED YOUR HELP!
If you are familiar with the ML-level of Isabelle, then
we can offer some money in order for you to write small parts
of the tutorial. Please get in contact with us (see addresses
on the webpage). If you are not familiar, but like to know
more about the bits and pieces that make up the Isabelle
code, then let us know what you are interested in or what
project you like to implement. Any constructive feedback
will be highly appreciated.

Anyway, enjoy the tutorial!

Best wishes,
Christian (on behalf of Larry and Michael)