--- a/CookBook/Intro.thy	Mon Jan 26 12:29:43 2009 +0000
+++ b/CookBook/Intro.thy	Mon Jan 26 16:09:02 2009 +0000
@@ -12,7 +12,7 @@
   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, 
-  feel free--you are very welcome!  
+  feel free---you are most welcome!  
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -62,11 +62,11 @@
 
 *}
 
-section {* Conventions in the Cookbook *}
+section {* Typographic Conventions *}
 
 text {*
 
-  All ML-code in this Cookbook is shown in highlighed displays, like the following 
+  All ML-code in this Cookbook is typeset in highlighed boxes, like the following 
   ML-expression.
 
   \begin{isabelle}
@@ -78,25 +78,28 @@
   \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 
+  This corresponds to how code can be processed inside the interactive
+  environment of Isabelle. It is therefore easy to experiment with the code
+  (which by the way is highly recommended). However, for better readability we
+  will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
   \isacharverbatimclose} and just write
 
+
   @{ML [display,gray] "3 + 4"}
   
-  for the code above. Whenever appropriate we also show the response of the code 
-  when evaluated. The response is prefixed with a @{text [quotes] ">"}" like
+  for the code above. Whenever appropriate we also show the response the code 
+  generates when evaluated. This 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}, 
+  The usual Isabelle commands are written in bold, for example \isacommand{lemma}, 
   \isacommand{foobar} and so on.  We use @{text "$"} to indicate that 
   a command  needs to be run on the Unix-command line, for example
 
   @{text [display] "$ ls -la"}
 
-  Pointers to further information and Isabelle files are highlighted 
+  Pointers to further information and Isabelle files are given 
   as follows:
 
   \begin{readmore}