--- a/CookBook/Readme.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Readme.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -2,11 +2,17 @@
 imports Base
 begin
 
-chapter {* Comments for Authors of the Cookbook *}
+chapter {* Comments for Authors *}
 
 text {*
 
   \begin{itemize}
+  \item The cookbook can be compiled on the command-line with:
+
+  \begin{center}
+  @{text "isabelle make"}
+  \end{center}
+
   \item You can include references to other Isabelle manuals using the 
   reference names from those manuals. To do this the following
   four latex commands are defined:
@@ -19,53 +25,62 @@
   \end{tabular}
   \end{center}
 
-  So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic 
+  So @{ML_text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for 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.
+  cookbook. They allow to check the written text against the current
+  Isabelle code and also allow to show responses of the ML-compiler.
   Therefore authors are strongly encouraged to use antiquotations wherever
-  it is appropriate.
+  appropriate.
   
-  The following antiquotations are in use:
+  The following antiquotations are defined:
 
   \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$] @{text "@{ML \"\<dots>\" for \<dots> in \<dots>}"} should be used for
+  displaying any ML-ex\-pression, because it checks whether the expression is valid
+  ML-code. The @{text "for"} and @{text "in"} arguments are optional. The
+  former is used for evaluating open expressions by giving a list of
+  free variables. The latter is used to indicate in which structure or structures the
+  ML-expression should be evaluated. Examples are:
+  
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "@{ML \"1 + 3\"}"}\\
+  @{text "@{ML \"a + b\" for a b}"}\\
+  @{text "@{ML Ident in OuterLex}"}
+  \end{tabular}
+  \end{center}
 
-  \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
+  \item[$\bullet$] @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} should be used to
+  display ML-ex\-pressions and their response.
+  The first expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the
   second is a pattern that specifies the result the first expression
-  produces. This specification can contain @{text [quotes] "\<dots>"} for parts that
-  can be omitted. The actual response will be checked against the
-  specification. For example @{text "@{ML_response \"(1+2,3)\"
+  produces. This specification can contain @{text "\<dots>"} for parts that
+  you like to omit. The response of the first expresion will be checked against 
+  this specification. An example is @{text "@{ML_response \"(1+2,3)\"
   \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be
-  constructed. It does not work when the code produces an exception or is an
-  abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
+  constructed: it does not work when the code produces an exception or returns 
+  an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
-  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like
+  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like
   the @{ML_text ML_response}-anti\-quotation, except that the
-  result-specification is not checked.
+  result-specification is not checked. Use this antiquotation 
+  if the result cannot be constructed or the code generates an exception.
 
-  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when
+  \item[$\bullet$] @{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.
+  environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, 
+  ensures that the environment markers are not printed.
 
-  \item Line numbers for code can be shown using 
-  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.
+  \item Line numbers can be printed using 
+  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
 
   \end{itemize}