theory Intro

imports Main

begin

chapter {* Introduction *}

text {*

  first steps in Isabelle programming, and to provide recipes for

  solving common problems. 

*}

section {* Intended Audience and Prior Knowledge *}

text {* 

  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}.

*}

text {*

  \begin{description}

  from a programmer's perspective, documenting both the underlying

  concepts and the concrete interfaces. 

  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.

  \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

  things (FIXME: need some short and convincing comment that this

  is a strategy, not a problem that should be solved).

*}

end