--- 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.