--- a/CookBook/Readme.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Readme.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -146,8 +146,9 @@
   the tutorial, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}
-  for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
+  \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}
+  for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The
+  tag is \isa{\%linenosgray} when the numbered text should be gray. 
 
   \end{itemize}