CookBook/Intro.thy
changeset 54 1783211b3494
parent 52 a04bdee4fb1e
child 60 5b9c6010897b
--- 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.
-
 *}