equal
deleted
inserted
replaced
75 unchanged. |
75 unchanged. |
76 |
76 |
77 \end{description} |
77 \end{description} |
78 |
78 |
79 All of the diagnostic commands above admit a list of @{text modes} |
79 All of the diagnostic commands above admit a list of @{text modes} |
80 to be specified, which is appended to the current print mode (see |
80 to be specified, which is appended to the current print mode; see |
81 also \cite{isabelle-ref}). Thus the output behavior may be modified |
81 \secref{sec:print-modes}. Thus the output behavior may be modified |
82 according particular print mode features. For example, @{command |
82 according particular print mode features. For example, @{command |
83 "pr"}~@{text "(latex xsymbols)"} would print the current proof state |
83 "pr"}~@{text "(latex xsymbols)"} would print the current proof state |
84 with mathematical symbols and special characters represented in |
84 with mathematical symbols and special characters represented in |
85 {\LaTeX} source, according to the Isabelle style |
85 {\LaTeX} source, according to the Isabelle style |
86 \cite{isabelle-sys}. |
86 \cite{isabelle-sys}. |