Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\

  Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\

  So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 

  \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used

  for displaying any ML-ex\-pression, because the antiquotation checks whether

  the expression is valid ML-code. The @{text "for"}- and @{text

  "in"}-arguments are optional. The former is used for evaluating open

  expressions by giving a list of free variables. The latter is used to

  indicate in which structure or structures the ML-expression should be

  evaluated. Examples are:

  \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}\\

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to

  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

  first expression will be checked against this pattern. Examples are:

  \begin{center}\small

  @{text "@{ML_response \"1+2\" \"3\"}"}\\

  @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}

  which produce respectively

  \begin{center}\small

  \begin{tabular}{p{3cm}p{3cm}}

  @{ML_response "1+2" "3"} &  

  @{ML_response "(1+2,3)" "(3,\<dots>)"}

  \end{tabular}

  \end{center}

  Note that this antiquotation can only be used when the result can be

  \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just

  like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,

  except that the result-specification is not checked. Use this antiquotation

  when the result cannot be constructed or the code generates an

  exception. Examples are:

  \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\"}"}

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be

  checked. An example is:

  \begin{center}\small

  \begin{tabular}{ll}

  @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\

                                    & @{text "\"Type unification failed \<dots>\"}"}

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when

  The listed antiquotations honour options including @{text "[display]"} and 

  @{text "[quotes]"}. For example

  \begin{center}\small

  @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}

  \end{center}

  while 

  \begin{center}\small

  @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}

  \end{center}

  environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 

  the Cookbook, however, ensures that the environment markers are not printed.