--- a/CookBook/Readme.thy	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/Readme.thy	Mon Feb 09 01:23:35 2009 +0000
@@ -7,12 +7,12 @@
 text {*
 
   \begin{itemize}
-  \item The Cookbook can be compiled on the command-line with:
+  \item This tutorial can be compiled on the command-line with:
 
   @{text [display] "$ isabelle make"}
 
   You very likely need a recent snapshot of Isabelle in order to compile
-  the Cookbook. Some parts of the Cookbook also rely on compilation with
+  the tutorial. Some parts of the tutorial also rely on compilation with
   PolyML.
 
   \item You can include references to other Isabelle manuals using the 
@@ -31,7 +31,7 @@
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for the 
-  Cookbook. They allow to check the written text against the current
+  tutorial. They allow to check the written text against the current
   Isabelle code and also allow to show responses of the ML-compiler.
   Therefore authors are strongly encouraged to use antiquotations wherever
   appropriate.
@@ -143,7 +143,7 @@
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
-  the Cookbook, however, ensures that the environment markers are not printed.
+  the tutorial, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
   \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}