--- a/CookBook/Intro.thy	Fri Jan 16 14:57:36 2009 +0000
+++ b/CookBook/Intro.thy	Fri Jan 23 17:50:35 2009 +0000
@@ -1,5 +1,5 @@
 theory Intro
-imports Main
+imports Base
 
 begin
 
@@ -8,24 +8,24 @@
 
 text {*
   The purpose of this Cookbook is to guide the reader through the first steps
-  of Isabelle programming, and to explain some tricks of the trade. The code
+  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.
+  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}.
+  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}.
 
 *}
 
@@ -67,8 +67,42 @@
 section {* Conventions *}
 
 text {*
-  We use @{text "$"} to indicate a command needs to be run on the Unix-command
-  line.
+
+  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}
+
 *}