--- a/ProgTutorial/FirstSteps.thy	Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 29 00:36:14 2009 +0200
@@ -1142,6 +1142,59 @@
   next section)
 *}
 
+section {* Setups (TBD) *}
+
+text {*
+  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 
+  @{ML_type "theory -> theory"}: the input theory is the current theory and the 
+  output the theory where the theory attribute has been stored.
+  
+  This is a fundamental principle in Isabelle. A similar situation occurs 
+  for example with declaring constants. The function that declares a 
+  constant on the ML-level is @{ML Sign.add_consts_i}. 
+  If you write\footnote{Recall that ML-code  needs to be 
+  enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
+*}  
+
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
+
+text {*
+  for declaring the constant @{text "BAR"} with type @{typ nat} and 
+  run the code, then you indeed obtain a theory as result. But if you 
+  query the constant on the Isabelle level using the command \isacommand{term}
+
+  \begin{isabelle}
+  \isacommand{term}~@{text [quotes] "BAR"}\\
+  @{text "> \"BAR\" :: \"'a\""}
+  \end{isabelle}
+
+  you do not obtain a constant of type @{typ nat}, but a free variable (printed in 
+  blue) of polymorphic type. The problem is that the ML-expression above did 
+  not register the declaration with the current theory. This is what the command
+  \isacommand{setup} is for. The constant is properly declared with
+*}
+
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
+
+text {* 
+  Now 
+  
+  \begin{isabelle}
+  \isacommand{term}~@{text [quotes] "BAR"}\\
+  @{text "> \"BAR\" :: \"nat\""}
+  \end{isabelle}
+
+  returns a (black) constant with the type @{typ nat}.
+
+  A similar command is \isacommand{local\_setup}, which expects a function
+  of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+  use the commands \isacommand{method\_setup} for installing methods in the
+  current theory and \isacommand{simproc\_setup} for adding new simprocs to
+  the current simpset.
+*}
+
 section {* Theorem Attributes *}
 
 text {*
@@ -1219,6 +1272,18 @@
   @{text "> "}~@{thm test[my_sym]}
   \end{isabelle}
 
+  An alternative for setting up an attribute is the function @{ML Attrib.setup}.
+  So instead of using \isacommand{attribute\_setup}, you can also set up the
+  attribute as follows:
+*}
+
+ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+  "applying the sym rule" *}
+
+text {*
+  This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
+  can be used for example with \isacommand{setup}.
+
   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
   as argument and resolve the proved theorem with this list (one theorem 
@@ -1510,58 +1575,6 @@
 *}
 
 
-section {* Setups (TBD) *}
-
-text {*
-  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 
-  @{ML_type "theory -> theory"}: the input theory is the current theory and the 
-  output the theory where the theory attribute has been stored.
-  
-  This is a fundamental principle in Isabelle. A similar situation occurs 
-  for example with declaring constants. The function that declares a 
-  constant on the ML-level is @{ML Sign.add_consts_i}. 
-  If you write\footnote{Recall that ML-code  needs to be 
-  enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
-*}  
-
-ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
-
-text {*
-  for declaring the constant @{text "BAR"} with type @{typ nat} and 
-  run the code, then you indeed obtain a theory as result. But if you 
-  query the constant on the Isabelle level using the command \isacommand{term}
-
-  \begin{isabelle}
-  \isacommand{term}~@{text [quotes] "BAR"}\\
-  @{text "> \"BAR\" :: \"'a\""}
-  \end{isabelle}
-
-  you do not obtain a constant of type @{typ nat}, but a free variable (printed in 
-  blue) of polymorphic type. The problem is that the ML-expression above did 
-  not register the declaration with the current theory. This is what the command
-  \isacommand{setup} is for. The constant is properly declared with
-*}
-
-setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
-
-text {* 
-  Now 
-  
-  \begin{isabelle}
-  \isacommand{term}~@{text [quotes] "BAR"}\\
-  @{text "> \"BAR\" :: \"nat\""}
-  \end{isabelle}
-
-  returns a (black) constant with the type @{typ nat}.
-
-  A similar command is \isacommand{local\_setup}, which expects a function
-  of type @{ML_type "local_theory -> local_theory"}. Later on we will also
-  use the commands \isacommand{method\_setup} for installing methods in the
-  current theory and \isacommand{simproc\_setup} for adding new simprocs to
-  the current simpset.
-*}
 
 section {* Theories, Contexts and Local Theories (TBD) *}