--- a/CookBook/Readme.thy	Fri Nov 28 05:19:55 2008 +0100
+++ b/CookBook/Readme.thy	Fri Nov 28 05:56:28 2008 +0100
@@ -23,17 +23,24 @@
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for the 
-  cookbook so that written text can be kept in sync with the 
+  cookbook. This allows to check the written text against the current
   Isabelle code and also that responses of the ML-compiler can be shown.
-  The are:
+  Therefore authors are strongly encouraged to use antiquotations wherever
+  it is appropriate.
+  
+  The following antiquotations are in use:
 
   \begin{itemize}
-  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value computations. It checks whether
-  the ML-expression is valid ML-code, but only works for closed expression.
-  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text ML}-antiquotation except, 
-  that  it can also deal with open expressions and expressions that need to be evaluated inside structures. 
-  The free variables or structures need to be listed after the @{ML_text "for"}. For example 
+  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value
+  computations. It checks whether the ML-expression is valid ML-code, but only
+  works for closed expression.
+
+  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text
+  ML}-antiquotation except, that it can also deal with open expressions and
+  expressions that need to be evaluated inside structures. The free variables
+  or structures need to be listed after the @{ML_text "for"}. For example
   @{text "@{ML_open \"a + b\" for a b}"}.
+
   \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} The first
   expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the
   second is a pattern that specifies the result the first expression
@@ -44,17 +51,22 @@
   constructed. It does not work when the code produces an exception or is an
   abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
-  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like the 
-  @{ML_text ML_response}-anti\-quotation, except that the result-specification is not
-  checked.
-  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when referring to a file. 
-  It checks whether the file exists.
+  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like
+  the @{ML_text ML_response}-anti\-quotation, except that the
+  result-specification is not checked.
+
+  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when
+  referring to a file. It checks whether the file exists.  
   \end{itemize}
 
+
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
   environments. Some \LaTeX-hack, however, does not print the environment markers.
 
+  \item Line numbers for code can be shown using 
+  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.
+
   \end{itemize}
 
 *}