theory Intro
imports Main
begin
chapter {* 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 (SML), 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 SML
\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}
The Cookbook is written in such a way that the code examples in it are
synchronised with fairly recent versions of the code.
*}
end