% $Id$
\chapter{Isabelle symbols}\label{app:symbols}
Isabelle supports an infinite number of non-ASCII symbols, which are
represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
identifier). It is left to front-end tools how these symbols are presented to
the user. The following predefined standard symbols are available by default
for Isabelle document output; most of these are also supported by
Proof~General when used together with the X-Symbol package.
\begin{center}
\input{syms}
\end{center}
Any symbol (or plain ASCII character) may be prefixed by a control sequence
\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript. E.g.\
\verb,A\<^sup>\<star>, is presented in {\LaTeX} as
\isa{A\isactrlsup{\isasymstar}}. See also Chapter~\ref{ch:present} for more
information on Isabelle document preparation and related issues.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
%%% End: