--- a/CookBook/Readme.thy	Sat Nov 01 15:20:36 2008 +0100
+++ b/CookBook/Readme.thy	Mon Nov 24 02:51:08 2008 +0100
@@ -7,7 +7,7 @@
 text {*
 
   \begin{itemize}
-  \item You can make references to other Isabelle manuals using the 
+  \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:
   
@@ -25,21 +25,40 @@
   \item There are various document antiquotations defined for the 
   cookbook so that written text can be kept in sync with the 
   Isabelle code and also that responses of the ML-compiler can be shown.
-  For example
+  The are:
 
   \begin{itemize}
-  \item[$\bullet$] @{text "@{ML \"\<dots>\"}"}
-  \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"}
-  \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"}
-  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\"}"}
-  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"}
+  \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
+  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)\"
+  \"(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}).
+
+  \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}
 
-  (FIXME: explain their usage)
+  \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.
 
   \end{itemize}
 
 *}
 
 
+
 end
\ No newline at end of file