1 theory Readme

     2 imports Base

     3 begin

     4 

     5 chapter {* Comments for Authors of the Cookbook *}

     6 

     7 text {*

     8 

     9   \begin{itemize}

    10   \item You can make references to other Isabelle manuals using the 

    11   reference names from those manuals. For this the following

    12   four latex commands are defined:

    13   

    14   \begin{center}

    15   \begin{tabular}{l|c|c}

    16    & Chapters & Sections\\\hline

    17   Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\

    18   Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\

    19   \end{tabular}

    20   \end{center}

    21 

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

    23   in the implementation manual, namely \ichcite{ch:logic}.

    24 

    25   \item There are various document antiquotations defined for the 

    26   cookbook so that written text can be kept in sync with the 

    27   Isabelle code and also that responses of the ML-compiler can be shown.

    28   For example

    29 

    30   \begin{itemize}

    31   \item[$\bullet$] @{text "@{ML \"\<dots>\"}"}

    32   \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"}

    33   \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"}

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

    35   \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"}

    36   \end{itemize}

    37 

    38   (FIXME: explain their usage)

    39 

    40   \end{itemize}

    41 

    42 *}

    43 

    44 

    45 end