--- a/CookBook/FirstSteps.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -171,11 +171,11 @@
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   The code about simpsets extracts the theorem names stored in the
-  current simpset.  We get hold of the current simpset with the antiquotation 
+  current simpset.  You can get hold of the current simpset with the antiquotation 
   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   containing all information about the simpset. The rules of a simpset are
   stored in a \emph{discrimination net} (a data structure for fast
-  indexing). From this net we can extract the entries using the function @{ML
+  indexing). From this net you can extract the entries using the function @{ML
   Net.entries}.
 
 
@@ -258,7 +258,7 @@
   @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
  
-  where an coercion is inserted in the second component and 
+  where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
@@ -345,7 +345,7 @@
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
-  Although to some extend types of terms can be inferred, there are many
+  Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function 
   type is as follows:
@@ -387,7 +387,7 @@
 
   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,
-  change every @{typ nat} into an @{typ int} using the function
+  change every @{typ nat} in a term into an @{typ int} using the function
 *}
 
 ML{*fun nat_to_int t =
@@ -411,7 +411,7 @@
 
 text {* 
   
-  You can freely construct and manipulate terms, since they are just
+  You can freely construct and manipulate @{ML_type "term"}s, since they are just
   arbitrary unchecked trees. However, you eventually want to see if a
   term is well-formed, or type-checks, relative to a theory.
   Type-checking is done via the function @{ML cterm_of}, which converts 
@@ -525,6 +525,8 @@
 
 section {* Storing Theorems *}
 
+text {* @{ML PureThy.add_thms_dynamic} *}
+
 section {* Theorem Attributes *}
 
 section {* Printing Terms and Theorems\label{sec:printing} *}
@@ -695,11 +697,11 @@
 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 one to read the code top-down.
+  composition allows you to read the code top-down.
 
   The remaining combinators described in this section add convenience for the
   ``waterfall method'' of writing functions. The combinator @{ML tap} allows
-  one to get hold of an intermediate result (to do some side-calculations for
+  you to get hold of an intermediate result (to do some side-calculations for
   instance). The function
 
  *}
@@ -709,12 +711,13 @@
        |> tap (fn x => tracing (makestring x))
        |> (fn x => x + 2)*}
 
-text {* increments the argument first by one and then by two. In the middle (Line 3),
-  however, it uses @{ML tap} for printing the ``plus-one'' intermediate 
-  result inside the tracing buffer. The function @{ML tap} can only
-  be used for side-calculations, because any value that is computed cannot
-  be merged back into the ``main waterfall''. To do this, you can use the next 
-  combinator.
+text {* 
+  increments the argument first by @{text "1"} and then by @{text "2"}. In the
+  middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+  intermediate result inside the tracing buffer. The function @{ML tap} can
+  only be used for side-calculations, because any value that is computed
+  cannot be merged back into the ``main waterfall''. To do this, you can use
+  the next combinator.
 
   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
   and returns the result together with the value (as a pair). For example
@@ -752,7 +755,7 @@
 ML{*fun (x, y) |-> f = f x y*}
 
 text {* and can be used to write the following roundabout version 
-  of the @{text double} function 
+  of the @{text double} function: 
 *}
 
 ML{*fun double x =
@@ -764,7 +767,7 @@
   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
-  for example, the function @{text double} can also be written as
+  for example, the function @{text double} can also be written as:
 *}
 
 ML{*val double =