theory Readme
imports Base
begin

chapter {* Comments for Authors of the Cookbook *}

text {*

  \begin{itemize}
  \item You can make 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 so that written text can be kept in sync with the 
  Isabelle code and also that responses of the ML-compiler can be shown.
  For example

  \begin{itemize}
  \item[$\bullet$] @{text "@{ML \"\<dots>\"}"}
  \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"}
  \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"}
  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\"}"}
  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"}
  \end{itemize}

  (FIXME: explain their usage)

  \end{itemize}

*}


end