diff -r 3e30ea95c7aa -r 009ca4807baa CookBook/Recipes/Config.thy
--- a/CookBook/Recipes/Config.thy	Wed Mar 11 17:38:17 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Mar 11 22:34:49 2009 +0000
@@ -12,9 +12,9 @@
 
   {\bf Solution:} This can be achieved using configuration values.\smallskip
 
-  Assume you want to control three values, namely @{text bval} containing a
+  Assume you want to control three values, say @{text bval} containing a
   boolean,  @{text ival} containing an integer and @{text sval} 
-  containing a string. These values can be declared on the ML-level with
+  containing a string. These values can be declared on the ML-level by
 *}
 
 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
@@ -23,7 +23,7 @@
 
 text {* 
   where each value needs to be given a default. To enable these values, they need to 
-  be set up by  
+  be set up with
 *}
 
 setup {* setup_bval *} 
@@ -51,18 +51,18 @@
 
   @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
 
-  The same can be achived using the command \isacommand{setup}.
+  The same can be achieved using the command \isacommand{setup}.
 *}
 
 setup {* Config.put_thy sval "bar" *}
 
 text {* 
-  The retrival of this value yields now
+  Now the retrival of this value yields:
 
   @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
 
   We can apply a function to a value using @{ML Config.map}. For example incrementing
-  @{ML ival} can be done by
+  @{ML ival} can be done by:
 
   @{ML_response [display,gray] 
 "let 
@@ -80,5 +80,4 @@
   multithreaded execution of Isabelle.
   
   *}
-
 end
\ No newline at end of file