--- a/CookBook/FirstSteps.thy	Fri Feb 20 23:19:41 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sat Feb 21 11:38:14 2009 +0000
@@ -658,11 +658,11 @@
 
   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
-  the name of the constant depends on the theory in which the term constructor
-  @{text "Nil"} is defined (@{text "List"}) and also in which datatype 
-  (@{text "list"}). Even worse, some constants have a name involving 
-  type-classes. Consider for example the constants for @{term "zero"} 
-  and @{text "(op *)"}:
+  the name of the constant @{term "Nil"} depends on the theory in which the
+  term constructor is defined (@{text "List"}) and also in which datatype
+  (@{text "list"}). Even worse, some constants have a name involving
+  type-classes. Consider for example the constants for @{term "zero"} and
+  @{text "(op *)"}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
  "(Const (\"HOL.zero_class.zero\", \<dots>), 
@@ -757,7 +757,7 @@
   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
   To calculate the type, this function traverses the whole term and will
-  detect any inconsistency. For examle changing the type of the variable 
+  detect any typing inconsistency. For examle changing the type of the variable 
   from @{typ "nat"} to @{typ "int"} will result in the error message: 
 
   @{ML_response_fake [display,gray] 
@@ -766,7 +766,7 @@
 
   Since the complete traversal might sometimes be too costly and
   not necessary, there is also the function @{ML fastype_of} which 
-  returns a type.
+  returns the type of a term.
 
   @{ML_response [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
@@ -797,7 +797,7 @@
   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 
   Instead of giving explicitly the type for the constant @{text "plus"} and the free 
-  variable @{text "x"}, the type-inference will fill in the missing information.
+  variable @{text "x"}, the type-inference filled in the missing information.
 
 
   \begin{readmore}
@@ -864,7 +864,7 @@
 
   However, while we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. So it cannot be referenced later
-  on. How to store theorems will be explained in the next section.
+  on. How to store theorems will be explained in Section~\ref{sec:storing}.
 
   \begin{readmore}
   For the functions @{text "assume"}, @{text "forall_elim"} etc 
@@ -913,7 +913,7 @@
 
 
 
-section {* Storing Theorems *}
+section {* Storing Theorems\label{sec:storing} *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}