diff -r d563f8ff6aa0 -r 5fbeeac2901b CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Mon Jan 12 16:03:05 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Jan 12 16:49:15 2009 +0000
@@ -562,8 +562,8 @@
   ProofGeneral. This results in some subtle configuration issues, which we
   will explain in this section.
 
-  Let us start with a ``silly'' command, below named \isacommand{foo}, which does nothing at all. 
-  On the ML-level it can be defined as
+  Let us start with a ``silly'' command, which we call \isacommand{foo} in what follows.
+  To keep things simple this command does nothing at all. On the ML-level it can be defined as
 
 @{ML [display]
 "let
@@ -574,7 +574,7 @@
 end"}
 
   The function @{ML OuterSyntax.command} expects a name for the command, a
-  short description, a flag (which we will explain it later on more thoroughly) and a
+  short description, a flag (which we will explain later on more thoroughly) and a
   parser for a top-level transition function (its purpose will also explained
   later). 
 
@@ -617,7 +617,7 @@
   For 
   our purposes it is sufficient to use the log files for the theories @{text "Pure"},
   @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
-  containing the new command. @{text Pure} and @{text HOL} are usually compiled during the 
+  containing the new \isacommand{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the 
   installation of Isabelle. So log files for them are already available. If not, then they 
   can be conveniently compiled using build-script from the distribution
 
@@ -648,11 +648,11 @@
 
   @{text [display] "use_thy \"Command\";"} 
   
-  to the file @{text "./FooCommand/ROOT.ML"}. Now we can compile the theory by just typing
+  to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing
 
   @{text [display] "$ isabelle make"}
 
-  We created now the necessary log files. They are typically stored 
+  We created finally all the necessary log files. They are typically stored 
   in the directory 
   
   @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
@@ -671,15 +671,15 @@
 Pure-ProofGeneral.gz
 HOL-FooCommand.gz"} 
 
-  We can now create the keyword file with
+  They are used for creating the keyword files with the command
 
 @{text [display]
 "$ isabelle keywords -k foo 
-       `$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral,HOL-FooCommand.gz}`"}
+       $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
 
-  The result is the file @{text "isar-keywords-foo.el"}, which needs to be 
+  The result is the file @{text "isar-keywords-foo.el"}. This file needs to be 
   copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
-  this keyword file, we need to start it with the option @{text "-k foo"}, i.e.
+  this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
 
   @{text [display] "isabelle -k foo <a-theory-file>"}
 
@@ -693,8 +693,7 @@
   OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
 end"}
 
-  then we can finally make use of \isacommand{foo}! Similarly
-  with any other command you want to implement. 
+  then we can make use of \isacommand{foo}! Similarly with any other new command. 
 
   In the example above, we built the theories on top of the HOL-logic. If you
   target other logics, such as Nominal or ZF, then you need to change the