--- a/CookBook/Base.thy	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/Base.thy	Mon Feb 09 01:23:35 2009 +0000
@@ -10,7 +10,7 @@
 
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
-    (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl)
+    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 *}

--- a/CookBook/Intro.thy	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/Intro.thy	Mon Feb 09 01:23:35 2009 +0000
@@ -8,19 +8,19 @@
 
 text {*
   If your next project requires you to program on the ML-level of Isabelle,
-  then this Cookbook is for you. It will guide you through the first steps of
+  then this tutorial is for you. It will guide you through the first steps of
   Isabelle programming, and also explain tricks of the trade. The best way to
   get to know the ML-level of Isabelle is by experimenting with the many code
-  examples included in the Cookbook. The code is as far as possible checked
+  examples included in the tutorial. The code is as far as possible checked
   against recent versions of Isabelle.  If something does not work, then
   please let us know. If you have comments, criticism or like to add to the
-  Cookbook, feel free---you are most welcome!
+  tutorial, feel free---you are most welcome!
 *}
 
 section {* Intended Audience and Prior Knowledge *}
 
 text {* 
-  This Cookbook targets readers who already know how to use Isabelle for
+  This tutorial targets readers who already know how to use Isabelle for
   writing theories and proofs. We also assume that readers are familiar with
   the functional programming language ML, the language in which most of
   Isabelle is implemented. If you are unfamiliar with either of these two
@@ -68,7 +68,7 @@
 
 text {*
 
-  All ML-code in this Cookbook is typeset in highlighted boxes, like the following 
+  All ML-code in this tutorial is typeset in highlighted boxes, like the following 
   ML-expression:
 
   \begin{isabelle}

--- 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>"}

--- a/CookBook/antiquote_setup.ML	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Mon Feb 09 01:23:35 2009 +0000
@@ -1,4 +1,4 @@
-(* Auxiliary antiquotations for the Cookbook. *)
+(* Auxiliary antiquotations for the tutorial. *)
 
 structure AntiquoteSetup: sig end =
 struct

--- a/CookBook/document/root.tex	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/document/root.tex	Mon Feb 09 01:23:35 2009 +0000
@@ -78,9 +78,9 @@
 \renewcommand{\isacharverbatimopen}{}%
 \renewcommand{\isacharverbatimclose}{}}{}
 
-\isakeeptag{CookBookML}
-\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
-\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}}
+\isakeeptag{TutorialML}
+\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
+\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers
@@ -103,7 +103,7 @@
 
 \title{\mbox{}\\[-10ex]
        \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
-       The Isabelle Programmer's Cookbook (fragment)}
+       The Isabelle Programming Tutorial (fragment)}
 
 \author{with contributions by:\\[2ex] 
         \begin{tabular}{r@{\hspace{1.8mm}}l}

--- a/IsaMakefile	Mon Feb 09 01:12:00 2009 +0000
+++ b/IsaMakefile	Mon Feb 09 01:23:35 2009 +0000
@@ -1,11 +1,11 @@
 
 ## targets
 
-default: cookbook
+default: tutorial
 images: 
 test: 
 
-all: cookbook
+all: tutorial
 
 ## global settings
 
@@ -21,7 +21,7 @@
 
 ## CookBook
 
-cookbook: CookBook/ROOT.ML \
+tutorial: CookBook/ROOT.ML \
           CookBook/document/root.tex \
           CookBook/document/root.bib \
           CookBook/*.thy \

Binary file cookbook.pdf has changed