diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Intro.thy --- 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. - *}