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