diff -r 065f472c09ab -r f3794c231898 CookBook/Readme.thy
--- a/CookBook/Readme.thy	Tue Dec 16 17:37:39 2008 +0100
+++ b/CookBook/Readme.thy	Tue Dec 16 17:28:05 2008 +0000
@@ -20,12 +20,12 @@
   \begin{center}
   \begin{tabular}{l|c|c}
    & Chapters & Sections\\\hline
-  Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\
-  Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\
+  Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\
+  Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\
   \end{tabular}
   \end{center}
 
-  So @{ML_text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 
+  So @{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 
@@ -37,50 +37,99 @@
   The following antiquotations are defined:
 
   \begin{itemize}
-  \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:
+  \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used
+  for displaying any ML-ex\-pression, because the antiquotation 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}\small
+  \begin{tabular}{lll}
+  @{text "@{ML \"1 + 3\"}"}         &         & @{ML "1 + 3"}\\
+  @{text "@{ML \"a + b\" for a b}"} & produce & @{ML "a + b" for a b}\\
+  @{text "@{ML Ident in OuterLex}"} &         & @{ML Ident in OuterLex}\\
+  \end{tabular}
+  \end{center}
+
+  \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to
+  display ML-expressions and their response.  The first expression is checked
+  like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern
+  that specifies the result the first expression produces. This pattern can
+  contain @{text "\<dots>"} for parts that you like to omit. The response of the
+  first expression will be checked against this pattern. Examples are:
+
+  \begin{center}\small
   \begin{tabular}{l}
-  @{text "@{ML \"1 + 3\"}"}\\
-  @{text "@{ML \"a + b\" for a b}"}\\
-  @{text "@{ML Ident in OuterLex}"}
+  @{text "@{ML_response \"1+2\" \"3\"}"}\\
+  @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}
   \end{tabular}
   \end{center}
 
-  \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 "\<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
+  which produce respectively
+
+  \begin{center}\small
+  \begin{tabular}{p{3cm}p{3cm}}
+  @{ML_response "1+2" "3"} &  
+  @{ML_response "(1+2,3)" "(3,\<dots>)"}
+  \end{tabular}
+  \end{center}
+  
+  Note that this antiquotation can only be used when the result can be
   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$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like
-  the @{ML_text ML_response}-anti\-quotation, except that the
-  result-specification is not checked. Use this antiquotation 
-  if the result cannot be constructed or the code generates an exception.
+  \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just
+  like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,
+  except that the result-specification is not checked. Use this antiquotation
+  when the result cannot be constructed or the code generates an
+  exception. Examples are:
+
+  \begin{center}\small
+  \begin{tabular}{ll}
+  @{text "@{ML_response"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\
+                          & @{text "\"a + b = c\"}"}\smallskip\\ 
+  @{text "@{ML_response"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ 
+                          & @{text "\"Exception FAIL raised\"}"}
+  \end{tabular}
+  \end{center}
+
   
-  \item[$\bullet$] @{text "@{ML_response_fake_both \"\<dots>\" \"\<dots>\"}"} can be
+  \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be
   used to show erroneous code. Neither the code nor the response will be
-  chacked.
+  checked. An example is:
 
-  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when
+  \begin{center}\small
+  \begin{tabular}{ll}
+  @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\
+                                    & @{text "\"Type unification failed \<dots>\"}"}
+  \end{tabular}
+  \end{center}
+
+  \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
   referring to a file. It checks whether the file exists.  
   \end{itemize}
 
+  The listed antiquotations honour options including @{text "[display]"} and 
+  @{text "[quotes]"}. For example
+
+  \begin{center}\small
+  @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
+  \end{center}
+
+  while 
+  
+  \begin{center}\small
+  @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
+  \end{center}
+  
+
 
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
-  environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, 
-  ensures that the environment markers are not printed.
+  environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
+  the Cookbook, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
   \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}