diff -r 02f76f1b6e7b -r dee4b3e66dfe CookBook/Intro.thy
--- a/CookBook/Intro.thy	Wed Oct 29 13:58:36 2008 +0100
+++ b/CookBook/Intro.thy	Wed Oct 29 21:46:33 2008 +0100
@@ -33,13 +33,18 @@
 
   \begin{description}
   \item[The Implementation Manual] describes Isabelle
-  from a programmer's perspective, documenting both the underlying
+  from a high-level perspective, documenting both the underlying
   concepts and some of the interfaces. 
 
   \item[The Isabelle Reference Manual] is an older document that used
-  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, particularly the chapters on tactics, are still useful.
+  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 
+  now, but some  parts, particularly the chapters on tactics, are still 
+  useful.
+
+  \item[The Isar Reference Manual] is also an older document that provides
+  material about Isar and its implementation. Some material in it
+  is still useful.
   \end{description}
 
   Then of course there is: