--- a/CookBook/Intro.thy	Mon Feb 16 17:17:24 2009 +0000
+++ b/CookBook/Intro.thy	Tue Feb 17 02:12:19 2009 +0000
@@ -15,7 +15,7 @@
   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
   tutorial, feel free---you are most welcome! The tutorial is meant to be 
-  gentle and comprehensive.
+  gentle and comprehensive. To achieve this we need your feedback.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -94,10 +94,10 @@
 
   @{ML_response [display,gray] "3 + 4" "7"}
 
-  The usual user-level commands of Isabelle 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 
-  in a Unix-shell, for example:
+  The user-level commands of Isabelle (i.e.~the non-ML code) are written
+  in bold, for example \isacommand{lemma}, \isacommand{apply},
+  \isacommand{foobar} and so on.  We use @{text "$"} to indicate that a
+  command needs to be run in a Unix-shell, for example:
 
   @{text [display] "$ ls -la"}
 
@@ -114,13 +114,15 @@
 
 text {*
   Financial support for this tutorial was provided by the German 
-  Research Council (DFG) under grant number URB 165/5-1.
+  Research Council (DFG) under grant number URB 165/5-1. The following
+  people contributed:
 
   \begin{itemize}
-  \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the 
-  \simpleinductive-package and the code for the @{text "chunk"}-antiquotation. He also wrote the first
-  version of the chapter describing the package and has be 
-  helpful \emph{beyond measure} with answering questions about Isabelle. 
+  \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
+  \simpleinductive-package and the code for the @{text
+  "chunk"}-antiquotation. He also wrote the first version of the chapter
+  describing the package and has been helpful \emph{beyond measure} with
+  answering questions about Isabelle.
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.