|
wenzelm@28838
|
1 |
theory Symbols
|
|
wenzelm@28838
|
2 |
imports Pure
|
|
wenzelm@28838
|
3 |
begin
|
|
wenzelm@28838
|
4 |
|
|
wenzelm@30045
|
5 |
chapter {* Predefined Isabelle symbols \label{app:symbols} *}
|
|
wenzelm@28838
|
6 |
|
|
wenzelm@28838
|
7 |
text {*
|
|
wenzelm@28838
|
8 |
Isabelle supports an infinite number of non-ASCII symbols, which are
|
|
wenzelm@28838
|
9 |
represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
|
|
wenzelm@28838
|
10 |
name}@{verbatim ">"} (where @{text name} may be any identifier). It
|
|
wenzelm@28838
|
11 |
is left to front-end tools how to present these symbols to the user.
|
|
wenzelm@28838
|
12 |
The collection of predefined standard symbols given below is
|
|
wenzelm@28838
|
13 |
available by default for Isabelle document output, due to
|
|
wenzelm@28838
|
14 |
appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
|
|
wenzelm@28838
|
15 |
name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
|
|
wenzelm@28838
|
16 |
">"} in the @{verbatim isabellesym.sty} file. Most of these symbols
|
|
wenzelm@28838
|
17 |
are displayed properly in Proof~General if used with the X-Symbol
|
|
wenzelm@28838
|
18 |
package.
|
|
wenzelm@28838
|
19 |
|
|
wenzelm@28838
|
20 |
Moreover, any single symbol (or ASCII character) may be prefixed by
|
|
wenzelm@28838
|
21 |
@{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
|
|
wenzelm@28838
|
22 |
"\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
|
|
wenzelm@28838
|
23 |
"A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
|
|
wenzelm@28838
|
24 |
versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
|
|
wenzelm@28838
|
25 |
"\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
|
|
wenzelm@28838
|
26 |
be used within identifiers. Sub- and superscripts that span a
|
|
wenzelm@28838
|
27 |
region of text are marked up with @{verbatim "\\"}@{verbatim
|
|
wenzelm@28838
|
28 |
"<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
|
|
wenzelm@28838
|
29 |
@{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
|
|
wenzelm@28838
|
30 |
"\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII
|
|
wenzelm@28838
|
31 |
characters and most other symbols may be printed in bold by
|
|
wenzelm@28838
|
32 |
prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
|
|
wenzelm@28838
|
33 |
"\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
|
|
wenzelm@28838
|
34 |
"\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
|
|
wenzelm@28838
|
35 |
\emph{not} be combined with sub- or superscripts for single symbols.
|
|
wenzelm@28838
|
36 |
|
|
wenzelm@28838
|
37 |
Further details of Isabelle document preparation are covered in
|
|
wenzelm@28838
|
38 |
\chref{ch:document-prep}.
|
|
wenzelm@28838
|
39 |
|
|
wenzelm@28838
|
40 |
\begin{center}
|
|
wenzelm@28838
|
41 |
\begin{isabellebody}
|
|
wenzelm@28838
|
42 |
\input{syms}
|
|
wenzelm@28838
|
43 |
\end{isabellebody}
|
|
wenzelm@28838
|
44 |
\end{center}
|
|
wenzelm@28838
|
45 |
*}
|
|
wenzelm@28838
|
46 |
|
|
wenzelm@28838
|
47 |
end |