--- a/CookBook/Intro.thy Mon Nov 24 02:51:08 2008 +0100
+++ b/CookBook/Intro.thy Tue Nov 25 05:19:27 2008 +0000
@@ -16,10 +16,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, the programming language in which
+ familiar with Standard ML (SML), the programming 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 Standard ML
+ tutorial \cite{isa-tutorial} or Paulson's book on SML
\cite{paulson-ml2}.
*}
@@ -57,12 +57,9 @@
learn from other people's code.
\end{description}
- Since Isabelle is not a finished product, these manuals, just like
- the implementation itself, are always under construction. This can
- be difficult and frustrating at times, especially when interfaces changes
- occur frequently. But it is a reality that progress means changing
- things (FIXME: need some short and convincing comment that this
- is a strategy, not a problem that should be solved).
+ The Cookbook is written in such a way that the code examples in it are
+ synchronised with fairly recent versions of the code.
+
*}