diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/Recipes/Config.thy Fri Jan 16 14:57:36 2009 +0000 @@ -12,7 +12,7 @@ {\bf Solution:} This can be achieved using configuration values.\smallskip - Assume you want to control three values, say @{ML_text bval} containing a + Assume you want to control three values, namely @{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 with *} @@ -23,7 +23,7 @@ text {* where each value needs to be given a default. To enable these values, they need to - be set up using + be set up by *} setup {* setup_bval *}