--- a/CookBook/FirstSteps.thy	Tue Jan 27 06:15:13 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Jan 27 17:50:08 2009 +0000
@@ -517,10 +517,11 @@
 
   \begin{readmore}
   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
-  and @{ML_file "Pure/General/basics.ML"}.
+  and @{ML_file "Pure/General/basics.ML"}. The section ?? in the implementation manual
+  contains also information about combinators.
   \end{readmore}
 
-  The simplest combinator is @{ML I} which is just the identity function.
+  The simplest combinator is @{ML I}, which is just the identity function.
 *}
 
 ML{*fun I x = x*}
@@ -530,7 +531,7 @@
 ML{*fun K x = fn _ => x*}
 
 text {*
-  It ``wraps'' a function around the argument @{text "x"}. However, this 
+  @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
   function ignores its argument. So @{ML K} defines a constant function 
   returning @{text x}.
 
@@ -578,7 +579,8 @@
 
 text {* 
   Another reason why the let-bindings in the code above are better to be
-  avoided: it is more than easy to get the intermediate values wrong!
+  avoided: it is more than easy to get the intermediate values wrong, not to 
+  mention the nightmares the maintenance of this code causes!
 
 
   (FIXME: give a real world example involving theories)
@@ -594,7 +596,8 @@
 
 text {* 
   which is the function composed of first the increment-by-one function and then
-  increment-by-two, followed by increment-by-three. 
+  increment-by-two, followed by increment-by-three. Again, the reverse function 
+  composition allows one to read the code top-down.
 
   The remaining combinators described in this section add convenience for the
   ``waterfall method'' of writing functions. The combinator @{ML tap} allows
@@ -608,9 +611,9 @@
        |> tap (fn x => tracing (makestring x))
        |> (fn x => x + 2)*}
 
-text {* increments the argument first by one and then by two. In the middle,
+text {* increments the argument first by one and then by two. In the middle (Line 3),
   however, it uses @{ML tap} for printing the ``plus-one'' intermediate 
-  result inside the tracing buffer (Line 3). The function @{ML tap} can only
+  result inside the tracing buffer. The function @{ML tap} can only
   be used for side-calculations, because any value that is computed cannot
   be merged back into the ``main waterfall''. To do this, the next combinator
   can be used.
@@ -661,8 +664,8 @@
   Recall that @{ML "|>"} is the reverse function applications. The related 
   reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"},
   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
-  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. In this
-  way, the function @{text double} can also be written as
+  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "|->"}, 
+  the function @{text double} can also be written as
 *}
 
 ML{*val double =

--- a/CookBook/Intro.thy	Tue Jan 27 06:15:13 2009 +0000
+++ b/CookBook/Intro.thy	Tue Jan 27 17:50:08 2009 +0000
@@ -11,7 +11,7 @@
   of Isabelle programming, and to explain tricks of the trade. The code
   provided in the Cookbook 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 or like to add to the Cookbook, 
+  know. If you have comments, criticism or like to add to the Cookbook, 
   feel free---you are most welcome!  
 *}
 

Binary file cookbook.pdf has changed