diff -r 4e2341f6599d -r fb8f22dd8ad0 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/FirstSteps.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -248,8 +248,8 @@
   avoided: it is more than easy to get the intermediate values wrong, not to 
   mention the nightmares the maintenance of this code causes!
 
-  A ``real world'' example for a function written in the waterfall fashion might
-  be the following:
+  In the context of Isabelle, a ``real world'' example for a function written in 
+  the waterfall fashion might be the following code:
 *}
 
 ML %linenosgray{*fun apply_fresh_args pred ctxt =
@@ -261,12 +261,12 @@
        |> (curry list_comb) pred *}
 
 text {*
-  The point of this function is to extract the argument types of the given
+  The point of this code is to extract the argument types of the given
   predicate and then generate for each type a distinct variable; finally it
   applies the generated variables to the predicate. You can read this off from
   how the function is coded: in Line 2, the function @{ML fastype_of}
   calculates the type of the predicate; in Line 3, @{ML binder_types} produces
-  the list of argument types; Line 4 pairs up each type with the string/name
+  the list of argument types; Line 4 pairs up each type with the string (or name)
   @{text "z"}; the function @{ML variant_frees in Variable} generates for each
   @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
   is turned into a list of variable terms in Line 6, which in the last line
@@ -782,9 +782,9 @@
       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
 end" "0 + 0"}
 
-  In Isabelle also types need can be certified. For example, you obtain
-  the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on the ML-level
-  as follows:
+  In Isabelle not just types need to be certified, but also types. For example, 
+  you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on 
+  the ML-level as follows:
 
   @{ML_response_fake [display,gray]
   "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
@@ -800,8 +800,8 @@
   result that type-checks.
   \end{exercise}
 
-  Remember that in Isabelle a term contains enough typing information
-  (constants, free variables and abstractions all have typing 
+  Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains 
+  enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
   Given a well-typed term, the function @{ML type_of} returns the 
   type of a term. Consider for example:
@@ -965,16 +965,16 @@
   an attribute.
 
   Before we can use the attribute, we need to set it up. This can be done
-  using the function @{ML Attrib.add_attributes} as follows.
+  using the function @{ML Attrib.setup} as follows.
 *}
 
-setup %gray {* Attrib.add_attributes 
-    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
+setup %gray {* Attrib.setup @{binding "my_sym"} 
+  (Scan.succeed my_symmetric) "applying the sym rule"*}
 
 text {*
   The attribute does not expect any further arguments (unlike @{text "[OF
   \<dots>]"}, for example, which can take a list of theorems as argument). Therefore
-  we use the function @{ML Attrib.no_args}. Later on we will also consider
+  we use the parser @{ML Scan.succeed}. Later on we will also consider
   attributes taking further arguments. An example for the attribute @{text
   "[my_sym]"} is the proof
 *} 
@@ -1035,9 +1035,8 @@
   and set up the attributes as follows
 *}
 
-setup %gray {* Attrib.add_attributes 
-          [("my_thms", Attrib.add_del_args my_add my_del, 
-              "maintaining a list of my_thms")] *}
+setup %gray {* Attrib.setup @{binding "my_thms"}
+  (Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}
 
 text {*
   Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
@@ -1165,13 +1164,62 @@
 *}
 
 
+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 functions from @{ML_type theory}
+  to @{ML_type 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}. Recall that ML-code 
+  needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
+  If you write 
+*}  
+
+ML{*Sign.add_consts_i [(Binding.name "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 with \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.name "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) *}
 
 text {*
-  (FIXME: expand)
-
-  (FIXME: explain \isacommand{setup})
-
   There are theories, proof contexts and local theories (in this order, if you
   want to order them). 
 
@@ -1182,10 +1230,7 @@
   @{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.
-
- *}
-
-
+*}
 
 section {* Storing Theorems\label{sec:storing} (TBD) *}