3 begin

     3 begin

     4 

     4 

     5 chapter {* Introduction *}

     5 chapter {* Introduction *}

     6 

     6 

     7 text {*

     7 text {*

     8   If your next project requires you to program on the ML-level of Isabelle,

    18   If your next project requires you to program on the ML-level of Isabelle,

     9   then this tutorial is for you. It will guide you through the first steps of

    19   then this tutorial is for you. It will guide you through the first steps of

    10   Isabelle programming, and also explain tricks of the trade. The best way to

    20   Isabelle programming, and also explain tricks of the trade. The best way to

    11   get to know the ML-level of Isabelle is by experimenting with the many code

    21   get to know the ML-level of Isabelle is by experimenting with the many code

    12   examples included in the tutorial. The code is as far as possible checked

    22   examples included in the tutorial. The code is as far as possible checked

    25   writing theories and proofs. We also assume that readers are familiar with

    35   writing theories and proofs. We also assume that readers are familiar with

    26   the functional programming language ML, the language in which most of

    36   the functional programming language ML, the language in which most of

    27   Isabelle is implemented. If you are unfamiliar with either of these two

    37   Isabelle is implemented. If you are unfamiliar with either of these two

    28   subjects, you should first work through the Isabelle/HOL tutorial

    38   subjects, you should first work through the Isabelle/HOL tutorial

    29   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.

    39   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.

    31 *}

    40 *}

    32 

    41 

    33 section {* Existing Documentation *}

    42 section {* Existing Documentation *}

    34 

    43 

    35 text {*

    44 text {*

    37   The following documentation about Isabelle programming already exists (and is

    45   The following documentation about Isabelle programming already exists (and is

    38   part of the distribution of Isabelle):

    46   part of the distribution of Isabelle):

    39 

    47 

    40   \begin{description}

    48   \begin{description}

    41   \item[The Isabelle/Isar Implementation Manual] describes Isabelle

    49   \item[The Isabelle/Isar Implementation Manual] describes Isabelle

    66   it is often also necessary to track the change history of a file or

    74   it is often also necessary to track the change history of a file or

    67   files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 

    75   files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 

    68   for Isabelle  provides convenient interfaces to query the history of

    76   for Isabelle  provides convenient interfaces to query the history of

    69   files and ``change sets''.

    77   files and ``change sets''.

    70   \end{description}

    78   \end{description}

    73 *}

    79 *}

    74 

    80 

    75 section {* Typographic Conventions *}

    81 section {* Typographic Conventions *}

    76 

    82 

    77 text {*

    83 text {*

    79   All ML-code in this tutorial is typeset in shaded boxes, like the following 

    84   All ML-code in this tutorial is typeset in shaded boxes, like the following 

    80   ML-expression:

    85   ML-expression:

    81 

    86 

    82   \begin{isabelle}

    87   \begin{isabelle}

    83   \begin{graybox}

    88   \begin{graybox}

   158   is no problem with updating your code after submission. At the moment

   163   is no problem with updating your code after submission. At the moment

   159   developers are not as diligent with checking their code against the AFP than

   164   developers are not as diligent with checking their code against the AFP than

   160   with checking agains the distribution, but generally problems will be caught

   165   with checking agains the distribution, but generally problems will be caught

   161   and the developer, who caused them, is expected to fix them. So also

   166   and the developer, who caused them, is expected to fix them. So also

   162   in this case code maintenance is done for you. 

   167   in this case code maintenance is done for you. 

   164 *}

   168 *}

   165 

   169 

   166 section {* Some Naming Conventions in the Isabelle Sources *}

   170 section {* Some Naming Conventions in the Isabelle Sources *}

   167 

   171 

   168 text {*

   172 text {*

   225   This document is still in the process of being written! All of the

   229   This document is still in the process of being written! All of the

   226   text is still under construction. Sections and 

   230   text is still under construction. Sections and 

   227   chapters that are under \underline{heavy} construction are marked 

   231   chapters that are under \underline{heavy} construction are marked 

   228   with TBD.}

   232   with TBD.}

   229 

   233 

   231   \vfill

   234   \vfill

   232   This document was compiled with:\\

   235   This document was compiled with:\\

   233   \input{version}\\

   236   \input{version}\\

   234   \input{pversion}

   237   \input{pversion}

   235 *}

   238 *}