chapter {* Comments for Authors *}

  \item The cookbook can be compiled on the command-line with:

  \begin{center}

  @{text "isabelle make"}

  \end{center}

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

  cookbook. They allow to check the written text against the current

  Isabelle code and also allow to show responses of the ML-compiler.

  appropriate.

  The following antiquotations are defined:

  \item[$\bullet$] @{text "@{ML \"\<dots>\" for \<dots> in \<dots>}"} should be used for

  displaying any ML-ex\-pression, because it 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{center}

  \begin{tabular}{l}

  @{text "@{ML \"1 + 3\"}"}\\

  @{text "@{ML \"a + b\" for a b}"}\\

  @{text "@{ML Ident in OuterLex}"}

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} should be used to

  display ML-ex\-pressions and their response.

  The first expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the

  produces. This specification can contain @{text "\<dots>"} for parts that

  you like to omit. The response of the first expresion will be checked against 

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

  constructed: it does not work when the code produces an exception or returns 

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

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

  result-specification is not checked. Use this antiquotation 

  if the result cannot be constructed or the code generates an exception.

  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when

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

  ensures that the environment markers are not printed.

  \item Line numbers can be printed using 

  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 

  for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.