diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/Config.thy --- 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