--- a/ProgTutorial/Parsing.thy	Mon Jun 18 16:46:38 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Jun 19 12:45:22 2012 +0900
@@ -397,7 +397,7 @@
   parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*}
 
 text {*
-  This parser corrsponds to the grammar:
+  This parser corresponds to the grammar:
 
   \begin{center}
   \begin{tabular}{lcl}
@@ -940,7 +940,7 @@
 
 text {*
   Often new commands, for example for providing new definitional principles,
-  need to be implemented. While this is not difficult on the ML-level and
+  need to be implemented. While this is not difficult on the ML-level and for
   jEdit, in order to be backwards compatible, new commands need also to be recognised 
   by Proof-General. This results in some subtle configuration issues, which we will 
   explain in the next section. Here we just describe how to define new commands
@@ -949,7 +949,7 @@
   Let us start with a ``silly'' command that does nothing at all. We
   shall name this command \isacommand{foobar}.  Before you can
   implement any new command, you have to ``announce'' it in the
-  \isacommand{keyword}-section of theory header. For \isacommand{foobar}
+  \isacommand{keywords}-section of your theory header. For \isacommand{foobar}
   we need to write something like
 
   \begin{graybox}
@@ -961,7 +961,7 @@
 
   whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
   command.  Another possible kind is @{text "thy_goal"}, or you can
-  also to omit the kind entirely, in which case you declare a keyword
+  also omit the kind entirely, in which case you declare a keyword
   (something that is part of a command).
 
   Now you can implement \isacommand{foobar} as follows.