diff -r e91f54791e14 -r 007e09485351 CookBook/Intro.thy
--- a/CookBook/Intro.thy	Tue Sep 09 14:57:23 2008 +0200
+++ b/CookBook/Intro.thy	Tue Sep 16 00:43:45 2008 +0200
@@ -15,8 +15,8 @@
 
 text {* 
   This cookbook targets an audience who already knows how to use Isabelle
-  for writing theories and proofs. It is also assumed that the reader is 
-  familiar with the \emph{Standard ML} programming language, in which  
+  for writing theories and proofs. We also assume that readers are 
+  familiar with the Standard ML, the programming language in which  
   most of Isabelle is implemented. If you are unfamiliar with any of
   these two subjects, you should first work through the Isabelle/HOL
   tutorial \cite{isa-tutorial} and Paulson's book on Standard ML
@@ -28,18 +28,18 @@
 
 text {*
   
-  The following documents about ML-coding for Isabelle already exist (they are
-  included in the Isabelle distribution):
+  The following documentation about Isabelle programming already exist (they are
+  included in the distribution of Isabelle):
 
   \begin{description}
   \item[The Implementation Manual] describes Isabelle
   from a programmer's perspective, documenting both the underlying
-  concepts and the concrete interfaces. 
+  concepts and some of the interfaces. 
 
   \item[The Isabelle Reference Manual] is an older document that used
-  to be the main reference, when all reasoning happened on the ML
-  level. Many parts of it are outdated now, but some parts, mainly the
-  chapters on tactics, are still useful.
+  to be the main reference at a time when all proof scripts were written 
+  on the ML level. Many parts of this manual are outdated now, but some 
+  parts, mainly the chapters on tactics, are still useful.
   \end{description}
 
   Then of ourse there is: