theory Readme
imports Base
begin

chapter {* Comments for Authors of the Cookbook *}

text {*

  \begin{itemize}
  \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:
  
  \begin{center}
  \begin{tabular}{l|c|c}
   & Chapters & Sections\\\hline
  Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\
  Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\
  \end{tabular}
  \end{center}

  So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic 
  in the implementation manual, namely \ichcite{ch:logic}.

  \item There are various document antiquotations defined for the 
  cookbook. This allows to check the written text against the current
  Isabelle code and also that responses of the ML-compiler can be shown.
  Therefore authors are strongly encouraged to use antiquotations wherever
  it is appropriate.
  
  The following antiquotations are in use:

  \begin{itemize}
  \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.  
  \end{itemize}


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

  \item Line numbers for code can be shown using 
  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.

  \end{itemize}

*}



end