--- a/CookBook/Intro.thy	Mon Jan 26 12:29:01 2009 +0000
+++ b/CookBook/Intro.thy	Mon Jan 26 12:29:43 2009 +0000
@@ -11,10 +11,8 @@
   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.  
-
+  know. If you have comments or like to add to the Cookbook, 
+  feel free--you are very welcome!  
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -64,11 +62,12 @@
 
 *}
 
-section {* Conventions *}
+section {* Conventions in the Cookbook *}
 
 text {*
 
-  All ML-code in this Cookbook is shown in highlighed displays, such as:
+  All ML-code in this Cookbook is shown in highlighed displays, like the following 
+  ML-expression.
 
   \begin{isabelle}
   \begin{graybox}
@@ -82,25 +81,26 @@
   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
+  \isacharverbatimclose} and just write
 
   @{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
+  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
 
   @{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
+  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 files are indicated as follows:
+  Pointers to further information and Isabelle files are highlighted 
+  as follows:
 
   \begin{readmore}
-  Further information.
+  Further information or pointer to file.
   \end{readmore}
 
 *}