--- a/CookBook/FirstSteps.thy	Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Mar 03 13:00:55 2009 +0000
@@ -406,13 +406,16 @@
   \emph{discrimination net} (a data structure for fast indexing). From this
   net you can extract the entries using the function @{ML Net.entries}.
   You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
-  in the current simpset---this simpset can be referred to using the antiquotation
+  in the current simpset. This simpset can be referred to using the antiquotation
   @{text "@{simpset}"}.
 
   @{ML_response_fake [display,gray] 
   "get_thm_names_from_ss @{simpset}" 
   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
+  Again, this way or referencing simpsets makes you independent from additions
+  of lemmas to the simpset by the user that potentially cause loops.
+
   \begin{readmore}
   The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
   and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
@@ -427,7 +430,7 @@
 
 text {*
   These bindings are difficult to maintain and also can be accidentally
-  overwritten by the user. This often breakes Isabelle
+  overwritten by the user. This often broke Isabelle
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
   usefulness in cases where data needs to be build up dynamically. In the
@@ -513,7 +516,7 @@
 *}
 
 
-section {* Constructing Terms and Types Manually *} 
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -568,13 +571,13 @@
 
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 
-text {* This can be equally written as: *}
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
 
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
   A handy function for manipulating terms is @{ML map_types}: it takes a 
-  function and applies it to every type in the term. You can, for example,
+  function and applies it to every type in a term. You can, for example,
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
@@ -918,7 +921,7 @@
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
   returns another theorem (namely @{text thm} resolved with the lemma 
   @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
-  an attribute (of type @{ML_type "attribute"}).
+  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.
@@ -974,7 +977,7 @@
 
 text {*
   These functions take a theorem and a context and, for what we are explaining
-  here it is sufficient to just return the context unchanged. They change
+  here it is sufficient that they just return the context unchanged. They change
   however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
   adds a theorem if it is not already included in the list, and @{ML
   Thm.del_thm} deletes one. Both functions use the predicate @{ML
@@ -982,7 +985,7 @@
   propositions (modulo alpha-equivalence).
 
 
-  We can turn both functions into attributes using
+  You can turn both functions into attributes using
 *}
 
 ML{*val my_add = Thm.declaration_attribute my_thms_add
@@ -1009,7 +1012,7 @@
   @{ML_response_fake [display,gray]
   "!my_thms" "[\"True\"]"}
 
-  We can also add theorems using the command \isacommand{declare}
+  You can also add theorems using the command \isacommand{declare}
 *}
 
 declare test[my_thms] trueI_2[my_thms add]
@@ -1030,7 +1033,7 @@
 
 declare test[my_thms del]
 
-text {* After this, the theorem list is: 
+text {* After this, the theorem list is again: 
 
   @{ML_response_fake [display,gray]
   "!my_thms"
@@ -1040,7 +1043,7 @@
   but there can be any number of them. We just have to change the parser for reading
   the arguments accordingly. 
 
-  However, as said at the beginning using references for storing theorems is
+  However, as said at the beginning of this example, using references for storing theorems is
   \emph{not} the received way of doing such things. The received way is to 
   start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
 *}
@@ -1052,7 +1055,7 @@
   fun merge _ = Thm.merge_thms) *}
 
 text {*
-  To use this data slot, we only have to change the functions @{ML my_thms_add} and
+  To use this data slot, you only have to change @{ML my_thms_add} and
   @{ML my_thms_del} to:
 *}
 
@@ -1083,7 +1086,7 @@
   modify the theorems.
 
   Furthermore, the facts are made available on the user level under the dynamic 
-  fact name @{text foo}. For example we can declare three lemmas to be of the kind
+  fact name @{text foo}. For example you can declare three lemmas to be of the kind
   @{text foo} by:
 *}
 
@@ -1103,7 +1106,7 @@
   @{text "> ?B"}
   \end{isabelle}
 
-  On the ML-level the rules marked with @{text "foo"} an be retrieved
+  On the ML-level the rules marked with @{text "foo"} can be retrieved
   using the function @{ML FooRules.get}:
 
   @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
@@ -1114,10 +1117,7 @@
   data.
   \end{readmore}
 
-  (FIXME What are: 
-
-  @{text "theory_attributes"}
-  @{text "proof_attributes"})
+  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
 
 
   \begin{readmore}