1 theory Intro

     2 imports Main

     3 

     4 begin

     5 

     6 chapter {* Introduction *}

     7 

     8 text {*

     9   The purpose of this document is to guide the reader through the

    10   first steps in Isabelle programming, and to provide recipes for

    11   solving common problems. 

    12 *}

    13 

    14 section {* Intended Audience and Prior Knowledge *}

    15 

    16 text {* 

    17   This cookbook targets an audience who already knows how to use the Isabelle

    18   system to write theories and proofs, but without using ML.

    19   You should also be familiar with the \emph{Standard ML} programming

    20   language, which is  used for Isabelle programming. If you are unfamiliar with any of

    21   these two subjects, you should first work through the Isabelle/HOL

    22   tutorial \cite{isa-tutorial} and Paulson's book on Standard ML

    23   \cite{paulson-ml2}.

    24 

    25 *}

    26 

    27 section {* Primary Documentation *}

    28 

    29 text {*

    30   

    31 

    32   \begin{description}

    33   \item[The Implementation Manual \cite{isa-imp}] describes Isabelle

    34   from a programmer's perspective, documenting both the underlying

    35   concepts and the concrete interfaces. 

    36 

    37   \item[The Isabelle Reference Manual \cite{isabelle-ref}] is an older document that used

    38   to be the main reference, when all reasoning happened on the ML

    39   level. Many parts of it are outdated now, but some parts, mainly the

    40   chapters on tactics, are still useful.

    41 

    42   \item[The code] is of course the ultimate reference for how

    43   things really work. Therefore you should not hesitate to look at the

    44   way things are actually implemented. More importantly, it is often

    45   good to look at code that does similar things as you want to do, to

    46   learn from other people's code.

    47   \end{description}

    48 

    49   Since Isabelle is not a finished product, these manuals, just like

    50   the implementation itself, are always under construction. This can

    51   be dificult and frustrating at times, when interfaces are changing

    52   frequently. But it is a reality that progress means changing

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

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

    55 *}

    56 

    57 

    58 end