diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -1365,7 +1365,8 @@
 
 text {*
   This gives a function from @{ML_type "theory -> theory"}, which
-  can be used for example with \isacommand{setup}.
+  can be used for example with \isacommand{setup} or with
+  @{ML "Context.>> o Context.map_theory"}.
 
   As an example of a slightly more complicated theorem attribute, we implement 
   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
@@ -1545,11 +1546,15 @@
   @{ML_type local_theory} is identical to the type of \emph{proof contexts}
   @{ML_type "Proof.context"}, although not every proof context constitutes a
   valid local theory.
+
+  @{ML "Context.>> o Context.map_theory"}
 *}
 
 section {* Setups (TBD) *}
 
 text {*
+  @{ML Sign.declare_const}
+
   In the previous section we used \isacommand{setup} in order to make
   a theorem attribute known to Isabelle. What happens behind the scenes
   is that \isacommand{setup} expects a function of type