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