equal
deleted
inserted
replaced
108 also \secref{sec:print-modes}. Thus the output behavior may be |
108 also \secref{sec:print-modes}. Thus the output behavior may be |
109 modified according particular print mode features. For example, |
109 modified according particular print mode features. For example, |
110 @{command "print_state"}~@{text "(latex xsymbols)"} prints the |
110 @{command "print_state"}~@{text "(latex xsymbols)"} prints the |
111 current proof state with mathematical symbols and special characters |
111 current proof state with mathematical symbols and special characters |
112 represented in {\LaTeX} source, according to the Isabelle style |
112 represented in {\LaTeX} source, according to the Isabelle style |
113 @{cite "isabelle-sys"}. |
113 @{cite "isabelle-system"}. |
114 |
114 |
115 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
115 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
116 systematic way to include formal items into the printed text |
116 systematic way to include formal items into the printed text |
117 document. |
117 document. |
118 \<close> |
118 \<close> |