[isabelle-dev] Isabelle Documentation Project

[Christian Urban]

Hi,

There is already quite good documentation available for users to learn how to
interact with Isabelle and to use it for proving theorems. However, the entry 
barrier for users to program on the ML-level of Isabelle is still unbearably 
high. We have money to change this state of affairs and want to provide a cook
book about ML-coding in Isabelle.

If you familiar with the ML-level of Isabelle, then then we can offer money 
for writing small parts of this documentation. Please get in contact with us. 
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. Above all we like to help future users and 
developers of Isabelle; we do not want to end up with some "artificial 
documentation" that is of nobody's help. We have outlined some possible
topics of interest at 

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

but we are more than welcome to the Isabelle community's input.

Best wishes,

Christian Urban
Larry Paulson
Michael Norrish