--- 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

--- a/CookBook/Recipes/Config.thy	Mon Jan 12 16:03:05 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Mon Jan 12 16:49:15 2009 +0000
@@ -14,7 +14,7 @@
 
   Assume you want to control three values, say @{ML_text bval} containing a
   boolean,  @{ML_text ival} containing an integer and @{ML_text sval} 
-  containing a string. These values can be declared on the ML-level by
+  containing a string. These values can be declared on the ML-level with
 *}
 
 ML {*
@@ -24,7 +24,7 @@
 *}
 
 text {* 
-  where each value is given a default. To enable these values, they need to 
+  where each value needs to be given a default. To enable these values, they need to 
   be set up using 
 *}
 
@@ -38,13 +38,13 @@
 *}
 
 text {*
-  The user can now manipulate the values with the command
+  The user can now manipulate the values from within Isabelle with the command
 *}
 
 declare [[bval = true, ival = 3]]
 
 text {*
-  from within Isabelle. On the ML-level these values can be retrieved using the 
+  On the ML-level these values can be retrieved using the 
   function @{ML Config.get}:
 
   @{ML_response [display] "Config.get @{context} bval" "true"}

--- a/CookBook/Recipes/TimeLimit.thy	Mon Jan 12 16:03:05 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Mon Jan 12 16:49:15 2009 +0000
@@ -11,7 +11,7 @@
   {\bf Solution:} This can be achieved using the function 
   @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume the following well-known function:
+  Assume the following infamous function:
 
   *}
 
@@ -27,7 +27,7 @@
 
   @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
 
-  takes a bit long. To avoid this, the call can be encapsulated 
+  takes a bit of time to finish. To avoid this, the call can be encapsulated 
   in a time limit of five seconds. For this you have to write:
 
 @{ML_response [display]

Binary file cookbook.pdf has changed