theory Introimports Mainbeginchapter {* Introduction *}text {* The purpose of this cookbook is to guide the reader through the first steps of Isabelle programming, and to provide recipes for solving common problems. *}section {* Intended Audience and Prior Knowledge *}text {* This cookbook targets an audience who already knows how to use Isabelle for writing theories and proofs. We also assume that readers are familiar with Standard ML, the programming language in which most of Isabelle is implemented. If you are unfamiliar with either of these two subjects, you should first work through the Isabelle/HOL tutorial \cite{isa-tutorial} or Paulson's book on Standard ML \cite{paulson-ml2}.*}section {* Existing Documentation *}text {* The following documentation about Isabelle programming already exists (and is part of the distribution of Isabelle): \begin{description} \item[The Implementation Manual] describes Isabelle from a high-level perspective, documenting both the underlying concepts and some of the interfaces. \item[The Isabelle Reference Manual] is an older document that used to be the main reference of Isabelle at a time when all proof scripts were written on the ML level. Many parts of this manual are outdated now, but some parts, particularly the chapters on tactics, are still useful. \item[The Isar Reference Manual] is also an older document that provides material about Isar and its implementation. Some material in it is still useful. \end{description} Then of course there is: \begin{description} \item[The code] is of course the ultimate reference for how things really work. Therefore you should not hesitate to look at the way things are actually implemented. More importantly, it is often good to look at code that does similar things as you want to do, to learn from other people's code. \end{description} Since Isabelle is not a finished product, these manuals, just like the implementation itself, are always under construction. This can be difficult and frustrating at times, especially when interfaces changes occur frequently. But it is a reality that progress means changing things (FIXME: need some short and convincing comment that this is a strategy, not a problem that should be solved).*}end