7 chapter {* Predefined Isabelle symbols \label{app:symbols} *}
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
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.
39 Further details of Isabelle document preparation are covered in
40 \chref{ch:document-prep}.