CookBook/Readme.thy
changeset 54 1783211b3494
parent 53 0c3580c831a4
child 58 f3794c231898
--- a/CookBook/Readme.thy	Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Readme.thy	Sat Dec 13 01:33:22 2008 +0000
@@ -15,7 +15,7 @@
 
   \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:
+  four \LaTeX{} commands are defined:
   
   \begin{center}
   \begin{tabular}{l|c|c}
@@ -44,7 +44,7 @@
   free variables. The latter is used to indicate in which structure or structures the
   ML-expression should be evaluated. Examples are:
   
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{l}
   @{text "@{ML \"1 + 3\"}"}\\
   @{text "@{ML \"a + b\" for a b}"}\\
@@ -67,6 +67,10 @@
   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_both \"\<dots>\" \"\<dots>\"}"} can be
+  used to show erroneous code. Neither the code nor the response will be
+  chacked.
 
   \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when
   referring to a file. It checks whether the file exists.