theory Intro+
−
imports Main+
−
+
−
begin+
−
+
−
chapter {* Introduction *}+
−
+
−
text {*+
−
  The purpose of this cookbook is to guide the reader through the+
−
  first steps in 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 the Standard ML, the programming language in which  +
−
  most of Isabelle is implemented. If you are unfamiliar with any of+
−
  these two subjects, you should first work through the Isabelle/HOL+
−
  tutorial \cite{isa-tutorial} and Paulson's book on Standard ML+
−
  \cite{paulson-ml2}.+
−
+
−
*}+
−
+
−
section {* Existing Documentation *}+
−
+
−
text {*+
−
  +
−
  The following documentation about Isabelle programming already exist (they are+
−
  included in the distribution of Isabelle):+
−
+
−
  \begin{description}+
−
  \item[The Implementation Manual] describes Isabelle+
−
  from a programmer's 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 at a time when all proof scripts were written +
−
  on the ML level. Many parts of this manual are outdated now, but some +
−
  parts, mainly the chapters on tactics, are still useful.+
−
  \end{description}+
−
+
−
  Then of ourse 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+
−