diff -r fbcb89d84ba6 -r a9eb69749c93 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Mar 30 15:23:19 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Mon Mar 30 17:40:20 2009 +0200
@@ -390,13 +390,13 @@
 
   produces three tokens where the first and the last are identifiers, since
   @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
-  other syntactic category.\footnote{Note that because of a possible a bug in
-  the PolyML runtime system the result is printed as @{text [quotes] "?"}, instead of
+  other syntactic category.\footnote{Note that because of a possible bug in
+  the PolyML runtime system, the result is printed as @{text [quotes] "?"}, instead of
   the tokens.} The second indicates a space.
 
   Many parsing functions later on will require spaces, comments and the like
   to have already been filtered out.  So from now on we are going to use the 
-  functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example:
+  functions @{ML filter} and @{ML OuterLex.is_proper} to do this. For example:
 
 @{ML_response_fake [display,gray]
 "let
@@ -423,7 +423,7 @@
  Token (\<dots>,(Keyword, \"|\"),\<dots>), 
  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 
-  you obtain a list consisting of only a command and two keyword tokens.
+  you obtain a list consisting of only one command and two keyword tokens.
   If you want to see which keywords and commands are currently known to Isabelle, type in
   the following code (you might have to adjust the @{ML print_depth} in order to
   see the complete list):
@@ -498,7 +498,7 @@
   parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). 
   Except that the error message of @{ML "OuterParse.!!!"} is fixed to be 
   @{text [quotes] "Outer syntax error"}
-  with a relatively precise description of the failure. For example:
+  together with a relatively precise description of the failure. For example:
 
 @{ML_response_fake [display,gray]
 "let 
@@ -520,7 +520,7 @@
   (FIXME: or give parser for numbers)
 
   Whenever there is a possibility that the processing of user input can fail, 
-  it is a good idea to give as much information about where the error 
+  it is a good idea to give all available information about where the error 
   occurred. For this Isabelle can attach positional information to tokens
   and then thread this information up the processing chain. To see this,
   modify the function @{ML filtered_input} described earlier to 
@@ -1014,7 +1014,7 @@
 text {*
   (FIXME: maybe move to after the tactic section)
 
-  Methods are a central to Isabelle. They are the ones you use for example
+  Methods are central to Isabelle. They are the ones you use for example
   in \isacommand{apply}. To print out all currently known methods you can use the 
   Isabelle command: