--- a/CookBook/FirstSteps.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/FirstSteps.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -79,8 +79,8 @@
   However this only works if the type of what is converted is monomorphic and is not 
   a function.
 
-  The funtion @{ML "warning"} should only be used for testing purposes, because any
-  output this funtion generates will be overwritten as soon as an error is
+  The function @{ML "warning"} should only be used for testing purposes, because any
+  output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
   function @{ML tracing} should be used. This function writes all output into
   a separate tracing buffer. For example
@@ -89,7 +89,7 @@
 
   It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
-  amounts of trace output. This rediretion can be achieved using the code
+  amounts of trace output. This redirection can be achieved using the code
 *}
 
 ML{* 
@@ -214,7 +214,7 @@
 
   Hint: The third term is already quite big, and the pretty printer
   may omit parts of it by default. If you want to see all of it, you
-  can use the following ML funtion to set the limit to a value high 
+  can use the following ML function to set the limit to a value high 
   enough:
   \end{exercise}
 
@@ -253,7 +253,7 @@
   While antiquotations are very convenient for constructing terms and types, 
   they can only construct fixed terms. Unfortunately, one often needs to construct terms
   dynamically. For example, a function that returns the implication 
-  @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
+  @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
   as arguments can only be written as
 *}
 
@@ -292,7 +292,7 @@
   The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
-  Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
+  Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   expansion automatically, for example:
 
   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}