--- a/CookBook/Intro.thy	Thu Jan 29 09:46:17 2009 +0000
+++ b/CookBook/Intro.thy	Thu Jan 29 09:46:36 2009 +0000
@@ -7,12 +7,14 @@
 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, criticism or like to add to the Cookbook, 
-  feel free---you are most welcome!  
+  If your next project requires you to program on the ML-level of Isabelle,
+  then this Cookbook is for you. It will guide you through the first steps of
+  Isabelle programming, and also explain tricks of the trade. The best way to
+  get to know the ML-level of Isabelle is by experimenting with the many code
+  examples included in the Cookbook. The code 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, criticism or like to add to the
+  Cookbook, feel free---you are most welcome!
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -41,7 +43,7 @@
 
   \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 
+  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.
 
@@ -56,8 +58,8 @@
   \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.
+  good to look at code that does similar things as you want to do and
+  to learn from other people's code.
   \end{description}
 
 *}
@@ -66,8 +68,8 @@
 
 text {*
 
-  All ML-code in this Cookbook is typeset in highlighed boxes, like the following 
-  ML-expression.
+  All ML-code in this Cookbook is typeset in highlighted boxes, like the following 
+  ML-expression:
 
   \begin{isabelle}
   \begin{graybox}
@@ -77,28 +79,28 @@
   \end{graybox}
   \end{isabelle}
   
-  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}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write
+  These boxes corresponds to how code can be processed inside the interactive
+  environment of Isabelle. It is therefore easy to experiment with what is 
+  displayed. However, for better readability we will drop the enclosing 
+  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:
 
 
   @{ML [display,gray] "3 + 4"}
   
-  for the code above. Whenever appropriate we also show the response the code 
+  Whenever appropriate we also show the response the code 
   generates when evaluated. This response is prefixed with a 
-  @{text [quotes] ">"} like
+  @{text [quotes] ">"} like:
 
   @{ML_response [display,gray] "3 + 4" "7"}
 
   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
+  a command  needs to be run in the Unix-shell, for example
 
   @{text [display] "$ ls -la"}
 
-  Pointers to further information and Isabelle files are given 
-  as follows:
+  Pointers to further information and Isabelle files are typeset in 
+  italic and highlighted as follows:
 
   \begin{readmore}
   Further information or pointer to file.