CookBook/Recipes/Config.thy
changeset 68 e7519207c2b7
parent 67 5fbeeac2901b
child 69 19106a9975c1
--- a/CookBook/Recipes/Config.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -75,16 +75,14 @@
   Config.get ctxt ival
 end" "4"}
 
-\begin{readmore}
+  \begin{readmore}
   For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
-\end{readmore}
+  \end{readmore}
 
-*}
-
-
-text {*
-
-  Note: Avoid to use references for this purpose!
+  There are many good reasons to control parameters in this way. One is
+  that it avoid global references, which cause many headaches with the
+  multithreaded execution of Isabelle.
+  
   *}
 
 end
\ No newline at end of file