5 chapter {* Comments for Authors *}

     5 chapter {* Comments for Authors *}

     6 

     6 

     7 text {*

     7 text {*

     8 

     8 

     9   \begin{itemize}

     9   \begin{itemize}

    11 

    11 

    12   \begin{center}

    12   \begin{center}

    13   @{text "isabelle make"}

    13   @{text "isabelle make"}

    14   \end{center}

    14   \end{center}

    15 

    15 

    16   You very likely need a recent snapshot of Isabelle in order to compile

    16   You very likely need a recent snapshot of Isabelle in order to compile

    18 

    18 

    19   \item You can include references to other Isabelle manuals using the 

    19   \item You can include references to other Isabelle manuals using the 

    20   reference names from those manuals. To do this the following

    20   reference names from those manuals. To do this the following

    21   four \LaTeX{} commands are defined:

    21   four \LaTeX{} commands are defined:

    22   

    22   

    30 

    30 

    31   So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 

    31   So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 

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

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

    33 

    33 

    34   \item There are various document antiquotations defined for the 

    34   \item There are various document antiquotations defined for the 

    36   Isabelle code and also allow to show responses of the ML-compiler.

    36   Isabelle code and also allow to show responses of the ML-compiler.

    37   Therefore authors are strongly encouraged to use antiquotations wherever

    37   Therefore authors are strongly encouraged to use antiquotations wherever

    38   appropriate.

    38   appropriate.

    39   

    39   

    40   The following antiquotations are defined:

    40   The following antiquotations are defined: