--- a/CookBook/FirstSteps.thy	Wed Mar 04 14:26:21 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Mar 05 16:46:43 2009 +0000
@@ -44,7 +44,7 @@
   evaluated by using the advance and undo buttons of your Isabelle
   environment. The code inside the \isacommand{ML}-command can also contain
   value and function bindings, and even those can be undone when the proof
-  script is retracted. As mentioned earlier, we will drop the
+  script is retracted. As mentioned in the Introduction, we will drop the
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
   show code. The lines prefixed with @{text [quotes] ">"} are not part of the
   code, rather they indicate what the response is when the code is evaluated.
@@ -73,14 +73,14 @@
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
   the function @{ML "warning"}. For example 
 
-  @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
+  @{ML_response [display,gray] "warning \"any string\"" "\"any string\""}
 
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, namely the function @{ML makestring}:
 
-  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
+  @{ML_response [display,gray] "warning (makestring 1)" "\"1\""} 
 
   However @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
@@ -91,7 +91,7 @@
   function @{ML tracing} is more appropriate. This function writes all output into
   a separate tracing buffer. For example:
 
-  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
+  @{ML_response [display,gray] "tracing \"foo\"" "\"foo\""}
 
   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 
@@ -429,12 +429,6 @@
   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
-  in @{ML_file "Pure/net.ML"}.
-  \end{readmore}
-
   While antiquotations have many applications, they were originally introduced in order 
   to avoid explicit bindings for theorems such as:
 *}
@@ -725,8 +719,10 @@
   the smallest name that is still unique, whereas @{ML base_name in Sign} always
   strips off all qualifiers.
 
+  (FIXME: These are probably now NameSpace functions)
+
   \begin{readmore}
-  FIXME
+  FIXME: Find the right files to do with naming.
   \end{readmore}
 *}
 
@@ -771,6 +767,19 @@
       (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:
+
+  @{ML_response_fake [display,gray]
+  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+  "nat \<Rightarrow> bool"}
+
+  \begin{readmore}
+  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
+  the file @{ML_file "Pure/thm.ML"}.
+  \end{readmore}
+
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type-checks.
@@ -830,7 +839,9 @@
 
   \begin{readmore}
   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-  checking and pretty-printing of terms are defined.
+  checking and pretty-printing of terms are defined. Fuctions related to the
+  type inference are implemented in @{ML_file "Pure/type.ML"} and 
+  @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 *}
 
@@ -1025,7 +1036,7 @@
   @{ML_response_fake [display,gray]
   "!my_thms" "[\"True\"]"}
 
-  You 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]