CookBook/Intro.thy
changeset 106 bdd82350cf22
parent 102 5e309df58557
child 107 258ce361ba1b
--- 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}