|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Symbols}% |
|
4 % |
|
5 \isadelimtheory |
|
6 \isanewline |
|
7 \isanewline |
|
8 % |
|
9 \endisadelimtheory |
|
10 % |
|
11 \isatagtheory |
|
12 \isacommand{theory}\isamarkupfalse% |
|
13 \ Symbols\isanewline |
|
14 \isakeyword{imports}\ Pure\isanewline |
|
15 \isakeyword{begin}% |
|
16 \endisatagtheory |
|
17 {\isafoldtheory}% |
|
18 % |
|
19 \isadelimtheory |
|
20 % |
|
21 \endisadelimtheory |
|
22 % |
|
23 \isamarkupchapter{Standard Isabelle symbols \label{app:symbols}% |
|
24 } |
|
25 \isamarkuptrue% |
|
26 % |
|
27 \begin{isamarkuptext}% |
|
28 Isabelle supports an infinite number of non-ASCII symbols, which are |
|
29 represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier). It |
|
30 is left to front-end tools how to present these symbols to the user. |
|
31 The collection of predefined standard symbols given below is |
|
32 available by default for Isabelle document output, due to |
|
33 appropriate definitions of \verb|\|\verb|isasym|\isa{name} for each \verb|\|\verb|<|\isa{name}\verb|>| in the \verb|isabellesym.sty| file. Most of these symbols |
|
34 are displayed properly in Proof~General if used with the X-Symbol |
|
35 package. |
|
36 |
|
37 Moreover, any single symbol (or ASCII character) may be prefixed by |
|
38 \verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\<star>|, for \isa{{\isachardoublequote}A\isactrlsup {\isasymstar}{\isachardoublequote}} the alternative |
|
39 versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may |
|
40 be used within identifiers. Sub- and superscripts that span a |
|
41 region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and |
|
42 \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively. Furthermore, all ASCII |
|
43 characters and most other symbols may be printed in bold by |
|
44 prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}. Note that \verb|\|\verb|<^bold>|, may |
|
45 \emph{not} be combined with sub- or superscripts for single symbols. |
|
46 |
|
47 Further details of Isabelle document preparation are covered in |
|
48 \chref{ch:document-prep}. |
|
49 |
|
50 \begin{center} |
|
51 \begin{isabellebody} |
|
52 \input{syms} |
|
53 \end{isabellebody} |
|
54 \end{center}% |
|
55 \end{isamarkuptext}% |
|
56 \isamarkuptrue% |
|
57 % |
|
58 \isadelimtheory |
|
59 % |
|
60 \endisadelimtheory |
|
61 % |
|
62 \isatagtheory |
|
63 \isacommand{end}\isamarkupfalse% |
|
64 % |
|
65 \endisatagtheory |
|
66 {\isafoldtheory}% |
|
67 % |
|
68 \isadelimtheory |
|
69 % |
|
70 \endisadelimtheory |
|
71 \end{isabellebody}% |
|
72 %%% Local Variables: |
|
73 %%% mode: latex |
|
74 %%% TeX-master: "root" |
|
75 %%% End: |