--- a/CookBook/FirstSteps.thy	Sat Feb 07 14:21:33 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sun Feb 08 08:45:25 2009 +0000
@@ -116,8 +116,9 @@
 
   @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
 
-  See leter on in Section~\ref{sec:printing} for information about printing 
-  out data of type @{ML_type term}, @{ML_type cterm} and @{ML_type thm}.
+  Section~\ref{sec:printing} will give more information about printing 
+  the main datas tructures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 
+  and @{ML_type thm}.
 *}
 
 
@@ -173,7 +174,7 @@
   current simpset.  We get hold of the current simpset with the antiquotation 
   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   containing all information about the simpset. The rules of a simpset are
-  stored in a \emph{discrimination net} (a datastructure for fast
+  stored in a \emph{discrimination net} (a data structure for fast
   indexing). From this net we can extract the entries using the function @{ML
   Net.entries}.
 
@@ -244,7 +245,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 function to set the limit to a value high 
+  can use the following ML-function to set the limit to a value high 
   enough:
 
   @{ML [display,gray] "print_depth 50"}
@@ -297,7 +298,7 @@
 
 text {*
   The reason is that you cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
+  @{term "tau"} into an antiquotation. For example the following does \emph{not} work.
 *}
 
 ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
@@ -344,14 +345,16 @@
 
   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
-  Similarly, you occasionally need to construct types manually. For example 
-  the function returning a function type is as follows:
+  Although to some extend types of terms can be inferred, there are many
+  situations where you need to construct types manually, especially  
+  when defining constants. For example the function returning a function 
+  type is as follows:
 
 *} 
 
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 
-text {* This can be equally written as *}
+text {* This can be equally written as: *}
 
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
@@ -483,7 +486,6 @@
   
   val Qt = implies_elim Pt_implies_Qt (assume assm2);
 in
-
   Qt 
   |> implies_intr assm2
   |> implies_intr assm1
@@ -520,20 +522,20 @@
 
 section {* Theorem Attributes *}
 
-section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
+section {* Printing Terms and Theorems\label{sec:printing} *}
 
 text {* 
-  During development, you will occationally feel the need to inspect terms, cterms 
-  or theorems. Isabelle contains elaborate pretty-printing functions for that, but 
-  for quick-and-dirty solutions they are way too unwieldy. A simple way to transform 
+  During development, you often want to inspect terms, cterms 
+  or theorems. Isabelle contains elaborate pretty-printing functions for printing them, 
+  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
   a term into a string is to use the function @{ML Syntax.string_of_term}.
 
   @{ML_response_fake [display,gray]
   "Syntax.string_of_term @{context} @{term \"1::nat\"}"
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
-  This produces a string, though with printing directions encoded in it. The string
-  can be properly printed, when enclosed in a @{ML warning}.
+  This produces a string with some printing directions encoded in it. The string
+  can be properly printed by using @{ML warning} foe example.
 
   @{ML_response_fake [display,gray]
   "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
@@ -608,10 +610,10 @@
   \begin{readmore}
   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
-  contains further information about them.
+  contains further information about combinators.
   \end{readmore}
 
-  The simplest combinator is @{ML I}, which is just the identity function.
+  The simplest combinator is @{ML I}, which is just the identity function defined as
 *}
 
 ML{*fun I x = x*}
@@ -623,7 +625,7 @@
 text {*
   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
   function ignores its argument. As a result, @{ML K} defines a constant function 
-  returning @{text x}.
+  always returning @{text x}.
 
   The next combinator is reverse application, @{ML "|>"}, defined as: 
 *}
@@ -641,7 +643,7 @@
     |> (fn x => x + 4)*}
 
 text {*
-  which increments the argument @{text x} by 5. It does this by first incrementing 
+  which increments its argument @{text x} by 5. It does this by first incrementing 
   the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
   the first component of the pair (Line 4) and finally incrementing the first 
   component by 4 (Line 5). This kind of cascading manipulations of values is quite