diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/Recipes/Config.thy
--- a/ProgTutorial/Recipes/Config.thy	Thu Oct 01 10:19:21 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-theory Config
-imports "../Base"
-begin
-
-section {* Configuration Options\label{rec:config} *} 
-
-text {*
-  {\bf Problem:} 
-  You would like to enhance your tool with options that can be changed 
-  by the user without having to resort to the ML-level.\smallskip
-
-  {\bf Solution:} This can be achieved using configuration values.\smallskip
-
-  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 by
-*}
-
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
-
-text {* 
-  where each value needs to be given a default. To enable these values, they need to 
-  be set up with
-*}
-
-setup {* setup_bval *} 
-setup {* setup_ival *}
-
-text {* or on the ML-level with *}
-
-ML{*setup_sval @{theory} *}
-
-text {*
-  The user can now manipulate the values from within Isabelle with the command
-*}
-
-declare [[bval = true, ival = 3]]
-
-text {*
-  On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}:
-
-  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
-
-  @{ML_response [display,gray] "Config.get @{context} ival" "3"}
-
-  The function @{ML Config.put} manipulates the values. For example
-
-  @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
-
-  The same can be achieved using the command \isacommand{setup}.
-*}
-
-setup {* Config.put_thy sval "bar" *}
-
-text {* 
-  Now the retrieval 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_response [display,gray] 
-"let 
-  val ctxt' = Config.map ival (fn i => i + 1) @{context}
-in 
-  Config.get ctxt' ival
-end" "4"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
-  \end{readmore}
-
-  There are many good reasons to control parameters in this way. One is
-  that no global reference is needed, which would cause many headaches 
-  with the multithreaded execution of Isabelle.
-*}
-
-end
\ No newline at end of file