diff -r 2a69b119cdee -r e91f54791e14 CookBook/Intro.thy
--- a/CookBook/Intro.thy	Sat Sep 06 04:32:18 2008 +0200
+++ b/CookBook/Intro.thy	Tue Sep 09 14:57:23 2008 +0200
@@ -6,7 +6,7 @@
 chapter {* Introduction *}
 
 text {*
-  The purpose of this document is to guide the reader through the
+  The purpose of this cookbook is to guide the reader through the
   first steps in Isabelle programming, and to provide recipes for
   solving common problems. 
 *}
@@ -14,31 +14,37 @@
 section {* Intended Audience and Prior Knowledge *}
 
 text {* 
-  This cookbook targets an audience who already knows how to use the Isabelle
-  system to write theories and proofs, but without using ML.
-  You should also be familiar with the \emph{Standard ML} programming
-  language, which is  used for Isabelle programming. If you are unfamiliar with any of
+  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  
+  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
   \cite{paulson-ml2}.
 
 *}
 
-section {* Primary Documentation *}
+section {* Existing Documentation *}
 
 text {*
   
+  The following documents about ML-coding for Isabelle already exist (they are
+  included in the Isabelle distribution):
 
   \begin{description}
-  \item[The Implementation Manual \cite{isa-imp}] describes Isabelle
+  \item[The Implementation Manual] describes Isabelle
   from a programmer's perspective, documenting both the underlying
   concepts and the concrete interfaces. 
 
-  \item[The Isabelle Reference Manual \cite{isabelle-ref}] is an older document that used
+  \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.
+  \end{description}
 
+  Then of ourse there is:
+
+  \begin{description}
   \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
@@ -48,8 +54,8 @@
 
   Since Isabelle is not a finished product, these manuals, just like
   the implementation itself, are always under construction. This can
-  be dificult and frustrating at times, when interfaces are changing
-  frequently. But it is a reality that progress means changing
+  be difficult and frustrating at times, especially when interfaces changes
+  occur frequently. But it is a reality that progress means changing
   things (FIXME: need some short and convincing comment that this
   is a strategy, not a problem that should be solved).
 *}