5 chapter {* Predefined Isabelle symbols \label{app:symbols} *}
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 if used with the X-Symbol
20 Moreover, any single symbol (or ASCII character) may be prefixed by
21 @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
22 "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
23 "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
24 versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
25 "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
26 be used within identifiers. Sub- and superscripts that span a
27 region of text are marked up with @{verbatim "\\"}@{verbatim
28 "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
29 @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
30 "\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII
31 characters and most other symbols may be printed in bold by
32 prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
33 "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
34 "\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
35 \emph{not} be combined with sub- or superscripts for single symbols.
37 Further details of Isabelle document preparation are covered in
38 \chref{ch:document-prep}.