diff -r d563f8ff6aa0 -r 5fbeeac2901b CookBook/Recipes/Config.thy
--- 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"}