--- a/CookBook/Intro.thy Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Intro.thy Sat Dec 13 01:33:22 2008 +0000
@@ -6,9 +6,10 @@
chapter {* Introduction *}
text {*
- The purpose of this cookbook is to guide the reader through the
+ The purpose of this Cookbook is to guide the reader through the
first steps of Isabelle programming, and to provide recipes for
- solving common problems.
+ solving common problems. The code provided in the Cookbook is
+ checked against recent versions of Isabelle.
*}
section {* Intended Audience and Prior Knowledge *}
@@ -16,10 +17,10 @@
text {*
This cookbook targets an audience who already knows how to use Isabelle
for writing theories and proofs. We also assume that readers are
- familiar with Standard ML (SML), the programming language in which
- most of Isabelle is implemented. If you are unfamiliar with either of
+ 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 subjects, you should first work through the Isabelle/HOL
- tutorial \cite{isa-tutorial} or Paulson's book on SML
+ tutorial \cite{isa-tutorial} or Paulson's book on ML
\cite{paulson-ml2}.
*}
@@ -57,9 +58,6 @@
learn from other people's code.
\end{description}
- The Cookbook is written in such a way that the code examples in it are
- checked against recent versions of the code.
-
*}