diff -r 7e04dc2368b0 -r 8d1a344a621e ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Mar 30 09:33:50 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Mar 31 15:48:53 2009 +0100
@@ -294,7 +294,7 @@
   avoided: it is more than easy to get the intermediate values wrong, not to 
   mention the nightmares the maintenance of this code causes!
 
-  In the context of Isabelle, a ``real world'' example for a function written in 
+  In Isabelle, a ``real world'' example for a function written in 
   the waterfall fashion might be the following code:
 *}
 
@@ -398,7 +398,8 @@
 
 ML{*fun (x, y) |-> f = f x y*}
 
-text {* and can be used to write the following roundabout version 
+text {* 
+  and can be used to write the following roundabout version 
   of the @{text double} function: 
 *}
 
@@ -406,13 +407,45 @@
       x |>  (fn x => (x, x))
         |-> (fn x => fn y => x + y)*}
 
+text {* 
+  The combinator @{ML ||>>} plays a central rôle whenever your task is to update a 
+  theory and the update also produces a side-result (for example a theorem). Functions 
+  for such tasks return a pair whose second component is the theory and the fist 
+  component is the side-result. Using @{ML ||>>}, you can do conveniently the update 
+  and also accumulate the side-results. Considder the following simple function. 
+*}
+
+ML %linenosgray{*fun acc_incs x =
+    x |> (fn x => ("", x)) 
+      ||>> (fn x => (x, x + 1))
+      ||>> (fn x => (x, x + 1))
+      ||>> (fn x => (x, x + 1))*}
+
+text {*
+  The purpose of Line 2 is to just pair up the argument with a dummy value (since
+  @{ML "||>>"} operates on pairs). Each of the next three lines just increment 
+  the value by one, but also nest the intrermediate results to the left. For example 
+
+  @{ML_response [display,gray]
+  "acc_incs 1"
+  "((((\"\", 1), 2), 3), 4)"}
+
+  You can continue this chain with:
+  
+  @{ML_response [display,gray]
+  "acc_incs 1 ||>> (fn x => (x, x + 2))"
+  "(((((\"\", 1), 2), 3), 4), 6)"}
+
+  (FIXME: maybe give a ``real world'' example)
+*}
+
 text {*
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related 
   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
-  @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
-  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
-  for example, the function @{text double} can also be written as:
+  @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} described above have related combinators for 
+  function composition, namely @{ML "#->"}, @{ML "#>>"}, @{ML "##>"} and @{ML "##>>"}. 
+  Using @{ML "#->"}, for example, the function @{text double} can also be written as:
 *}
 
 ML{*val double =