--- a/ProgTutorial/FirstSteps.thy	Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sat Nov 07 01:03:37 2009 +0100
@@ -91,6 +91,9 @@
   However, both commands will only play minor roles in this tutorial (we will
   always arrange that the ML-code is defined outside proofs).
 
+  
+
+
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
   theory by using the command \isacommand{use}. For example
@@ -542,8 +545,27 @@
 text {* 
   which is the function composed of first the increment-by-one function and then
   increment-by-two, followed by increment-by-three. Again, the reverse function 
-  composition allows you to read the code top-down.
+  composition allows you to read the code top-down. This combinator is often used
+  for setup function inside the \isacommand{setup}-command. These function have to be
+  of type @{ML_type "theory -> theory"} in order to install, for example, some new 
+  data inside the current theory. More than one such setup function can be composed 
+  with @{ML "#>"}. For example
+*}
 
+setup %gray {* let
+  val (ival1, setup_ival1) = Attrib.config_int "ival1" 1
+  val (ival2, setup_ival2) = Attrib.config_int "ival2" 2
+in
+  setup_ival1 #>
+  setup_ival2
+end *}
+
+text {*
+  after this the configuration values @{text ival1} and @{text ival2} are known
+  in the current theory and can be manipulated by the user (for more information 
+  about configuration values see Section~\ref{sec:storing}, for more about setup 
+  functions see Section~\ref{sec:theories}). 
+  
   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
@@ -814,6 +836,21 @@
   under this name (this becomes especially important when you deal with
   theorem lists; see Section \ref{sec:storing}).
 
+  It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
+  whose first argument is a statement (possibly many of them separated by @{text "and"},
+  and the second is a proof. For example
+*}
+
+ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *}
+
+text {*
+  which can be printed out as follows
+
+  @{ML_response_fake [gray,display]
+"foo_thm |> string_of_thms @{context}
+         |> tracing"
+  "True, True"}
+
   You can also refer to the current simpset via an antiquotation. To illustrate 
   this we implement the function that extracts the theorem names stored in a 
   simpset.