theory Intro
imports Base

begin


chapter {* Introduction *}

text {*
  The purpose of this Cookbook is to guide the reader through the first steps
  of Isabelle programming, and to explain tricks of the trade. The code
  provided in the Cookbook is as far as possible checked against recent
  versions of Isabelle.  If something does not work, then please let us
  know. If you have comments or like to add to the Cookbook, you are very
  welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly 
  updated.  

*}

section {* Intended Audience and Prior Knowledge *}

text {* 
  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}.

*}

section {* Existing Documentation *}

text {*
  
  The following documentation about Isabelle programming already exists (and is
  part of the distribution of Isabelle):

  \begin{description}
  \item[The Implementation Manual] describes Isabelle
  from a high-level perspective, documenting both the underlying
  concepts and some of the interfaces. 

  \item[The Isabelle Reference Manual] is an older document that used
  to be the main reference of Isabelle at a time when all proof scripts 
  were written on the ML level. Many parts of this manual are outdated 
  now, but some  parts, particularly the chapters on tactics, are still 
  useful.

  \item[The Isar Reference Manual] is also an older document that provides
  material about Isar and its implementation. Some material in it
  is still useful.
  \end{description}

  Then of course there is:

  \begin{description}
  \item[The code] is of course the ultimate reference for how
  things really work. Therefore you should not hesitate to look at the
  way things are actually implemented. More importantly, it is often
  good to look at code that does similar things as you want to do, to
  learn from other people's code.
  \end{description}

*}

section {* Conventions *}

text {*

  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}

*}


end