equal
deleted
inserted
replaced
180 \isadelimML |
180 \isadelimML |
181 % |
181 % |
182 \endisadelimML |
182 \endisadelimML |
183 % |
183 % |
184 \begin{isamarkuptext}% |
184 \begin{isamarkuptext}% |
185 \noindent The X-Symbol package within Proof~General provides several |
185 \noindent Proof~General provides several input methods to enter |
186 input methods to enter \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may |
186 \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may just type a named |
187 just type a named entity \verb,\,\verb,<oplus>, by hand; the |
187 entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will |
188 corresponding symbol will be displayed after further input. |
188 be displayed after further input. |
189 |
189 |
190 More flexible is to provide alternative syntax forms |
190 More flexible is to provide alternative syntax forms |
191 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By |
191 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By |
192 convention, the mode of ``$xsymbols$'' is enabled whenever |
192 convention, the mode of ``$xsymbols$'' is enabled whenever |
193 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |
193 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |