Antiquotation setup is now contained in theory Base.
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 the 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} 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, particularly the chapters on tactics, are 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+ −