equal
deleted
inserted
replaced
146 (*<*) |
146 (*<*) |
147 setup {* Sign.local_path *} |
147 setup {* Sign.local_path *} |
148 (*>*) |
148 (*>*) |
149 |
149 |
150 text {* |
150 text {* |
151 \noindent The X-Symbol package within Proof~General provides several |
151 \noindent Proof~General provides several input methods to enter |
152 input methods to enter @{text \<oplus>} in the text. If all fails one may |
152 @{text \<oplus>} in the text. If all fails one may just type a named |
153 just type a named entity \verb,\,\verb,<oplus>, by hand; the |
153 entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will |
154 corresponding symbol will be displayed after further input. |
154 be displayed after further input. |
155 |
155 |
156 More flexible is to provide alternative syntax forms |
156 More flexible is to provide alternative syntax forms |
157 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By |
157 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By |
158 convention, the mode of ``$xsymbols$'' is enabled whenever |
158 convention, the mode of ``$xsymbols$'' is enabled whenever |
159 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |
159 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |