--- 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: