34 text {* 

    34 text {* 

    35   This tutorial targets readers who already know how to use Isabelle for

    35   This tutorial targets readers who already know how to use Isabelle for

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

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

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

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

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

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

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

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

    41 *}

    41 *}

    42 

    42 

    43 section {* Existing Documentation *}

    43 section {* Existing Documentation *}

    44 

    44 

    66   \begin{description}

    66   \begin{description}

    67   \item[The Isabelle sources.] They are the ultimate reference for how

    67   \item[The Isabelle sources.] They are the ultimate reference for how

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

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

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

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

    70   good to look at code that does similar things as you want to do and

    70   good to look at code that does similar things as you want to do and

    72   often your best friend while programming with Isabelle, or

    73   often your best friend while programming with Isabelle, or

    73   hypersearch if you program using jEdit under MacOSX. To understand the sources,

    74   hypersearch if you program using jEdit under MacOSX. To understand the sources,

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

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

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

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

    76   for Isabelle  provides convenient interfaces to query the history of

    77   for Isabelle  provides convenient interfaces to query the history of

    80 

    81 

    81 section {* Typographic Conventions *}

    82 section {* Typographic Conventions *}

    82 

    83 

    83 text {*

    84 text {*

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

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

    86 

    87 

    87   \begin{isabelle}

    88   \begin{isabelle}

    88   \begin{graybox}

    89   \begin{graybox}

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

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

    90   \hspace{5mm}@{ML "3 + 4"}\isanewline

    91   \hspace{5mm}@{ML "3 + 4"}\isanewline

   131 

   132 

   132 section {* Aaaaargh! My Code Does not Work Anymore *}

   133 section {* Aaaaargh! My Code Does not Work Anymore *}

   133 

   134 

   134 text {*

   135 text {*

   135   One unpleasant aspect of any code development inside a larger system is that

   136   One unpleasant aspect of any code development inside a larger system is that

   137   update lets potentially all hell break loose, because other developers have

   138   update lets potentially all hell break loose, because other developers have

   138   changed code you are relying on. Cursing is somewhat helpful in such situations, 

   139   changed code you are relying on. Cursing is somewhat helpful in such situations, 

   139   but taking the view that incompatible code changes are a fact of life 

   140   but taking the view that incompatible code changes are a fact of life 

   140   might be more gratifying. Isabelle is a research project. In most circumstances 

   141   might be more gratifying. Isabelle is a research project. In most circumstances 

   141   it is just impossible to make research backward compatible (imagine Darwin 

   142   it is just impossible to make research backward compatible (imagine Darwin 

   142   attempting to make the Theory of Evolution backward compatible).

   143   attempting to make the Theory of Evolution backward compatible).

   143 

   144 

   169 *}

   170 *}

   170 

   171 

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

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

   172 

   173 

   173 text {*

   174 text {*

   206 

   207 

   207   \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.

   208   \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.

   208 

   209 

   209   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 

   210   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 

   210   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 

   211   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 

   212   are by him.

   213   are by him.

   213 

   214 

   214   \item {\bf Jeremy Dawson} wrote the first version of the chapter

   215   \item {\bf Jeremy Dawson} wrote the first version of the chapter

   215   about parsing.

   216   about parsing.

   216 

   217