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
