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. It is also assumed that the reader is
familiar with the \emph{Standard ML} 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 documents about ML-coding for Isabelle already exist (they are
included in the Isabelle distribution):
\begin{description}
\item[The Implementation Manual] describes Isabelle
from a programmer's perspective, documenting both the underlying
concepts and the concrete interfaces.
\item[The Isabelle Reference Manual] is an older document that used
to be the main reference, when all reasoning happened on the ML
level. Many parts of it 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