added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
theory Readmeimports Basebeginchapter {* 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. For 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