--- a/CookBook/Parsing.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/Parsing.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -11,7 +11,7 @@
   Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so
   on, belong to the outer syntax, whereas items inside double quotation marks, such 
   as terms, types and so on, belong to the inner syntax. For parsing inner syntax, 
-  Isabelle uses a rather general and sophisticated algorithm due to Earley, which 
+  Isabelle uses a rather general and sophisticated algorithm, which 
   is driven by priority grammars. Parsers for outer syntax are built up by functional
   parsing combinators. These combinators are a well-established technique for parsing, 
   which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
@@ -348,7 +348,7 @@
 
 text {*
   Most of the time, however, Isabelle developers have to deal with parsing
-  tokens, not strings.  These token parsers will have the type:
+  tokens, not strings.  These token parsers have the type:
 *}
   
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
@@ -406,7 +406,7 @@
 *}
 
 ML{*fun filtered_input str = 
-       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
+  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
 
 text {*
 
@@ -594,14 +594,14 @@
   The functions to do with input and output of XML and YXML are defined 
   in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
   \end{readmore}
+  
 *}
 
-
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 
 text {*
   There are a number of special purpose parsers that help with parsing
-  specifications of functions, inductive definitions and so on. In
+  specifications of function definitions, inductive predicates and so on. In
   Capter~\ref{chp:package}, for example, we will need to parse specifications
   for inductive predicates of the form:
 *}
@@ -613,6 +613,8 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
+text {* and *}
+
 simple_inductive 
   trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
@@ -692,8 +694,8 @@
 *}
 
 text {*
-  Whenever types are given, they are stored in the @{ML SOME}s. They types are
-  not yet given to the variable: this must be done by type inference later
+  Whenever types are given, they are stored in the @{ML SOME}s. The types are
+  not yet used to type the variables: this must be done by type-inference later
   on. Since types are part of the inner syntax they are strings with some
   encoded information (see previous section). If a syntax translation is
   present for a variable, then it is stored in the @{ML Mixfix} datastructure;
@@ -853,7 +855,7 @@
 
   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
  
-  on the Unix prompt. If you now also type @{text "ls $ISABELLE_LOGS"}, then the 
+  on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the 
   directory should include the files:
 
   @{text [display]