102 |
102 |
103 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, |
103 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, |
104 |
104 |
105 \end{enumerate} |
105 \end{enumerate} |
106 |
106 |
107 Here $ident$ may be any identifier according to the usual Isabelle |
107 Here $ident$ is any sequence of letters. |
108 conventions. This results in an infinite store of symbols, whose |
108 This results in an infinite store of symbols, whose |
109 interpretation is left to further front-end tools. For example, the |
109 interpretation is left to further front-end tools. For example, the |
110 user-interface of Proof~General + X-Symbol and the Isabelle document |
110 user-interface of Proof~General + X-Symbol and the Isabelle document |
111 processor (see \S\ref{sec:document-preparation}) display the |
111 processor (see \S\ref{sec:document-preparation}) display the |
112 \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}. |
112 \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}. |
113 |
113 |
118 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
118 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
119 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
119 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
120 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
120 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
121 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
121 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
122 output as \isa{A\isactrlsup {\isasymstar}}. |
122 output as \isa{A\isactrlsup {\isasymstar}}. |
|
123 |
|
124 A number of symbols are considered letters by the Isabelle lexer |
|
125 and can be used as part of identifiers. These are the greek letters |
|
126 \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from |
|
127 \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}} |
|
128 (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), |
|
129 and the special control symbols \verb+\+\verb+<^isub>+ and |
|
130 \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This |
|
131 means that the input |
|
132 |
|
133 \medskip |
|
134 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,} |
|
135 |
|
136 \medskip |
|
137 \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}} |
|
138 by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like |
|
139 \isa{PA}, not an exponentiation. |
|
140 |
123 |
141 |
124 \medskip Replacing our definition of \isa{xor} by the following |
142 \medskip Replacing our definition of \isa{xor} by the following |
125 specifies an Isabelle symbol for the new operator:% |
143 specifies an Isabelle symbol for the new operator:% |
126 \end{isamarkuptext}% |
144 \end{isamarkuptext}% |
127 \isamarkuptrue% |
145 \isamarkuptrue% |