--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,57 @@
+theory Config
+imports Base
+begin
+
+section {* Configuration Options *} 
+
+
+text {*
+  {\bf Problem:} 
+  You would like to enhance your tool with options which can be changed later on
+  by the user.\smallskip
+
+  {\bf Solution:} This can be achieved using configuration values.\smallskip
+
+  *}
+
+ML {*
+val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false
+val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0
+val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string"
+*}
+
+setup "setup_bvalue o setup_ivalue o setup_svalue"
+
+declare [[bvalue = true, ivalue = 3]]
+
+text {*
+  Note that this works without introducing a new command to modify the 
+  configuration options. *}
+
+ML {*
+Config.get @{context} bvalue
+*}
+
+ML {*
+Config.get_thy @{theory} ivalue
+*}
+
+setup {* Config.put_thy svalue "foo" *}
+
+ML {* 
+Config.get @{context} svalue
+*}
+
+ML {*
+let val ctxt = Config.map ivalue (fn i => i + 1) @{context}
+in Config.get ctxt ivalue end
+*}
+
+
+text {*
+  Code: Pure/Isar/attrib.ML, Pure/config.ML
+
+  Note: Avoid to use references for this purpose!
+  *}
+
+end
\ No newline at end of file