\item You can include references to other Isabelle manuals using the 

  The are:

  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value computations. It checks whether

  the ML-expression is valid ML-code, but only works for closed expression.

  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} Works like @{ML_text ML}-antiquotation except, 

  that  it can also deal with open expressions and expressions that need to be evaluated inside structures. 

  The free variables or structures need to be listed after the @{ML_text "for"}. For example 

  @{text "@{ML_open \"a + b\" for a b}"}.

  \item[$\bullet$] {\bf @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}} 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 [quotes] "\<dots>"} for parts that

  can be omitted. The actual response will be checked against the

  specification. For example @{text "@{ML_response \"(1+2,3)\"

  \"(3,\<dots>)\"}"}. This antiquotation can only be used when the result can be

  constructed. It does not work when the code produces an exception or is an

  abstract datatype (like @{ML_type thm} or @{ML_type cterm}).

  \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like the 

  @{ML_text ML_response}-anti\-quotation, except that the result-specification is not

  checked.

  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when referring to a file. 

  It checks whether the file exists.

  \item Functions and value bindings cannot be defined inside antiquotations; they need

  to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}

  environments. Some \LaTeX-hack, however, does not print the environment markers.