diff -r 141751cab5b2 -r dfbd535cd1fd ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Wed Oct 26 13:19:09 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Thu Oct 27 18:11:52 2011 +0100
@@ -489,14 +489,34 @@
   then increment-by-two, followed by increment-by-three. Again, the reverse
   function composition allows you to read the code top-down. This combinator
   is often used for setup functions inside the
-  \isacommand{setup}-command. These functions have to be of type @{ML_type
-  "theory -> theory"}. More than one such setup function can be composed with
-  @{ML "#>"}.\footnote{TBD: give example} 
-  
-  The remaining combinators we describe in this section add convenience for the
-  ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
-  Basics} allows you to get hold of an intermediate result (to do some
-  side-calculations or print out an intermediate result, for instance). The function
+  \isacommand{setup}- or \isacommand{local\_setup}-command. These functions 
+  have to be of type @{ML_type "theory -> theory"}, respectively 
+  @{ML_type "local_theory -> local_theory"}. More than one such setup function 
+  can be composed with @{ML "#>"}. Consider for example the following code, 
+  where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1} 
+  and @{thm [source] conjunct2} under alternative names.
+*}  
+
+local_setup %graylinenos {* 
+let  
+  fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd
+in
+  my_note @{binding "foo_conjI"} @{thm conjI} #>
+  my_note @{binding "bar_conjunct1"} @{thm conjunct1} #>
+  my_note @{binding "bar_conjunct2"} @{thm conjunct2}
+end *}
+
+text {*
+  The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
+  @{ML_ind note in Local_Theory}; its purpose is to store a theorem under a name. 
+  In lines 5 to 6 we call this function to give alternative names for three
+  theorems. The point of @{ML "#>"} is that you can sequence such functions. 
+
+  The remaining combinators we describe in this section add convenience for
+  the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
+  in Basics} allows you to get hold of an intermediate result (to do some
+  side-calculations or print out an intermediate result, for instance). The
+  function
  *}
 
 ML %linenosgray{*fun inc_by_three x =
@@ -624,9 +644,33 @@
   "acc_incs 1 ||>> (fn x => (x, x + 2))"
   "(((((\"\", 1), 2), 3), 4), 6)"}
 
-  \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}
+  An example for this combinator is for example the following code
+*}
+
+ML {*
+val (((one_def, two_def), three_def), ctxt') = 
+  @{context}
+  |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
+  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
+  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
 *}
 
+ML {*
+  @{context}
+  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
+  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
+  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
+*}
+
+ML {*
+  val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = 
+  @{context}
+  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
+  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
+  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
+*}
+
+
 text {*
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related reverse function composition is @{ML "#>"}. In fact all the