theory Readme
imports Base
begin

chapter {* Comments for Authors *}

text {*

  \begin{itemize}
  \item The cookbook can be compiled on the command-line with:

  \begin{center}
  @{text "isabelle make"}
  \end{center}

  \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}"} yields 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. They allow to check the written text against the current
  Isabelle code and also allow to show responses of the ML-compiler.
  Therefore authors are strongly encouraged to use antiquotations wherever
  appropriate.
  
  The following antiquotations are defined:

  \begin{itemize}
  \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}\small
  \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
  second is a pattern that specifies the result the first expression
  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)\"
  \"(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 returns 
  an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).

  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like
  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 \"\<dots>\" \"\<dots>\"}"} can be
  used to show erroneous code. Neither the code nor the response will be
  chacked.

  \item[$\bullet$] @{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. 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.

  \end{itemize}

*}



end