--- a/CookBook/FirstSteps.thy	Fri Oct 10 17:13:56 2008 +0200
+++ b/CookBook/FirstSteps.thy	Mon Oct 13 17:51:09 2008 +0200
@@ -182,8 +182,8 @@
 section {* Terms and Types *}
 
 text {*
-  One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
-  @{text "@{term \<dots>}"}:
+  One way to construct terms of Isabelle on the ML level is by using the antiquotation 
+  \mbox{@{text "@{term \<dots>}"}}:
 *}
 
 ML {* @{term "(a::nat) + b = c"} *}
@@ -193,7 +193,7 @@
   representation of this term. This internal representation corresponds to the 
   datatype @{ML_text "term"}.
   
-  The internal representation of terms uses the usual de-Bruijn index mechanism where bound 
+  The internal representation of terms uses the usual de Bruijn index mechanism where bound 
   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
   binds the corresponding variable. However, in Isabelle the names of bound variables are 
@@ -501,7 +501,7 @@
   (FIXME: Pointer to the old reference manual)
   \end{readmore}
 
-  While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
+  While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
   are expected to leave the conclusion @{term C} intact, with the 
   exception of possibly instantiating schematic variables.