imports Base

  of Isabelle programming, and to explain tricks of the trade. The code

  welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly 

  updated.  

  This Cookbook targets readers who already know how to use Isabelle for

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

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

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

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

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

  All ML-code in this Cookbook is shown in highlighed displays, such as:

  \begin{isabelle}

  \begin{graybox}

  \isa{\isacommand{ML}

  \isacharverbatimopen\isanewline

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

  \isacharverbatimclose}

  \end{graybox}

  \end{isabelle}

  This corresponds to how code can be processed inside the interactive 

  environment of Isabelle. However, for better readability we will drop 

  the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots 

  \isacharverbatimclose} and just show

  @{ML [display,gray] "3 + 4"}

  for the code above. Whenever appropriate we show the response of the code 

  when evaluated. The response is prefixed with a @{text [quotes] ">"}", like

  @{ML_response [display,gray] "3 + 4" "7"}

  Isabelle commands are written in bold. For example \isacommand{lemma}, 

  \isacommand{foobar} and so on.  We use @{text "$"} to indicate a command 

  needs to be run on the Unix-command line, like

  @{text [display] "$ ls -la"}

  Pointers to further information and files are indicated as follows:

  \begin{readmore}

  Further information.

  \end{readmore}