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