6 

     6 

     7 chapter {* Introduction *}

     7 chapter {* Introduction *}

     8 

     8 

     9 text {*

     9 text {*

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

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

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

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

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

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

    15   against recent versions of Isabelle.  If something does not work, then

    15   against recent versions of Isabelle.  If something does not work, then

    16   please let us know. If you have comments, criticism or like to add to the

    16   please let us know. If you have comments, criticism or like to add to the

    18 *}

    18 *}

    19 

    19 

    20 section {* Intended Audience and Prior Knowledge *}

    20 section {* Intended Audience and Prior Knowledge *}

    21 

    21 

    22 text {* 

    22 text {* 

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

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

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

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

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

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

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

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

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

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

    66 

    66 

    67 section {* Typographic Conventions *}

    67 section {* Typographic Conventions *}

    68 

    68 

    69 text {*

    69 text {*

    70 

    70 

    72   ML-expression:

    72   ML-expression:

    73 

    73 

    74   \begin{isabelle}

    74   \begin{isabelle}

    75   \begin{graybox}

    75   \begin{graybox}

    76   \isacommand{ML}~@{text "\<verbopen>"}\isanewline

    76   \isacommand{ML}~@{text "\<verbopen>"}\isanewline