diff -r 0c3580c831a4 -r 1783211b3494 CookBook/Readme.thy --- 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 \"\\" \"\\"}"} can be + used to show erroneous code. Neither the code nor the response will be + chacked. \item[$\bullet$] @{text "@{ML_file \"\\"}"} Should be used when referring to a file. It checks whether the file exists.