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