--- a/CookBook/Readme.thy	Tue Dec 16 17:28:05 2008 +0000
+++ b/CookBook/Readme.thy	Wed Dec 17 05:08:33 2008 +0000
@@ -13,6 +13,9 @@
   @{text "isabelle make"}
   \end{center}
 
+  You very likely need a recent snapshot of Isabelle in order to compile
+  the cookbook.
+
   \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:
@@ -47,9 +50,9 @@
   
   \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}\\
+  @{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}
 
@@ -57,7 +60,7 @@
   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
+  contain @{text [quotes] "\<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
@@ -88,14 +91,25 @@
 
   \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\"}"}
+  @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\
+                               & @{text "\"a + b = c\"}"}\smallskip\\ 
+  @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ 
+                               & @{text "\"Exception FAIL raised\"}"}
   \end{tabular}
   \end{center}
 
+  which produce respectively
+
+  \begin{center}\small
+  \begin{tabular}{p{7.2cm}}
+  @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
+  @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
+  \end{tabular}
+  \end{center}
   
+  This output mimics to some extend what the user sees when running the
+  code.
+
   \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be
   used to show erroneous code. Neither the code nor the response will be
   checked. An example is:
@@ -108,7 +122,10 @@
   \end{center}
 
   \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
-  referring to a file. It checks whether the file exists.  
+  referring to a file. It checks whether the file exists.  An example
+  is 
+
+  @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
   \end{itemize}
 
   The listed antiquotations honour options including @{text "[display]"} and 
@@ -118,7 +135,7 @@
   @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
   \end{center}
 
-  while 
+  whereas
   
   \begin{center}\small
   @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}