|
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 Isabelle/jEdit and {\LaTeX} generated from Isabelle. |
|
18 |
|
19 Moreover, any single symbol (or ASCII character) may be prefixed by |
|
20 @{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript, |
|
21 such as @{verbatim "A\<^sup>\<star>"} for @{text "A\<^sup>\<star>"} and @{verbatim "A\<^sub>1"} for |
|
22 @{text "A\<^sub>1"}. Sub- and superscripts that span a region of text can |
|
23 be marked up with @{verbatim "\<^bsub>"}@{text "\<dots>"}@{verbatim |
|
24 "\<^esub>"} and @{verbatim "\<^bsup>"}@{text "\<dots>"}@{verbatim "\<^esup>"} |
|
25 respectively, but note that there are limitations in the typographic |
|
26 rendering quality of this form. Furthermore, all ASCII characters |
|
27 and most other symbols may be printed in bold by prefixing |
|
28 @{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for @{text "\<^bold>\<alpha>"}. Note that |
|
29 @{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined. |
|
30 |
|
31 Further details of Isabelle document preparation are covered in |
|
32 \chref{ch:document-prep}. |
|
33 |
|
34 \begin{center} |
|
35 \begin{isabellebody} |
|
36 \input{syms} |
|
37 \end{isabellebody} |
|
38 \end{center} |
|
39 *} |
|
40 |
|
41 end |