doc-src/System/symbols.tex

HOL/record: shared operations ("more", "fields", etc.) now need to be
always qualified;

% $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 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.

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

See also Chapter~\ref{ch:present} for more details on Isabelle document
preparation.

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

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