doc-src/System/symbols.tex

\<^bsub> .. \<^esub>

% $Id$

\chapter{Standard 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 to present these symbols to
the user.  The collection of predefined standard symbols given below is
available by default for Isabelle document output, due to appropriate
definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the
\verb,isabellesym.sty, file.  Most of these symbols are displayed properly in
Proof~General if used with the X-Symbol package.

Moreover, any single symbol (or ASCII character) may be prefixed by
\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,,
such as \verb,\<^bold>\<alpha>, for \isa{\isactrlbold{\isasymalpha}}.  Note
that super- and subscripts may \emph{not} be combined with bold style.

Further details of Isabelle document preparation are covered in
chapter~\ref{ch:present}.

\begin{center}
  \begin{isabellebody}
    \input{syms}  
  \end{isabellebody}
\end{center}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "system"
%%% End: