diff -r 0fb5f91d5109 -r 624279d187e1 CookBook/FirstSteps.thy
--- 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 =