--- a/CookBook/FirstSteps.thy	Tue Jan 27 21:22:27 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 28 06:29:16 2009 +0000
@@ -381,6 +381,8 @@
   number representing their sum.
   \end{exercise}
 
+
+  (FIXME: operation from page 19 of the implementation manual)
 *}
 
 section {* Type-Checking *}
@@ -429,6 +431,8 @@
   result that type-checks.
   \end{exercise}
 
+  (FIXME: @{text "ctyp_of"})
+
 *}
 
 section {* Theorems *}
@@ -503,6 +507,8 @@
 text {*
 
 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
+
+  authentic syntax
   
 *}
 
@@ -531,7 +537,7 @@
 
 text {*
   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
-  function ignores its argument. So @{ML K} defines a constant function 
+  function ignores its argument. As a result @{ML K} defines a constant function 
   returning @{text x}.
 
   The next combinator is reverse application, @{ML "|>"}, defined as 
@@ -585,7 +591,7 @@
   (FIXME: give a real world example involving theories)
 
   Similarly, the combinator @{ML "#>"} is the reverse function 
-  composition. It can be used to define functions as follows
+  composition. It can be used to define the following function
 *}
 
 ML{*val inc_by_six = 
@@ -660,11 +666,11 @@
         |-> (fn x => fn y => x + y)*}
 
 text {*
-  Recall that @{ML "|>"} is the reverse function applications. The related 
-  reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"},
+  Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
+  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 "|->"}, 
-  the function @{text double} can also be written as
+  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
+  for example, the function @{text double} can also be written as
 *}
 
 ML{*val double =