doc-src/System/symbols.tex
 author wenzelm Wed Jan 02 21:54:45 2002 +0100 (2002-01-02) changeset 12619 ddfe8083fef2 parent 12465 47f79ad602d9 child 14894 d23f6b505e9a permissions -rw-r--r--
tuned;
     1

     2 % $Id$

     3

     4 \chapter{Standard Isabelle symbols}\label{app:symbols}

     5

     6 Isabelle supports an infinite number of non-ASCII symbols, which are

     7 represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any

     8 identifier).  It is left to front-end tools how to present these symbols to

     9 the user.  The collection of predefined standard symbols given below is

    10 available by default for Isabelle document output, due to appropriate

    11 definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the

    12 \verb,isabellesym.sty, file.  Most of these symbols are displayed properly in

    13 Proof~General if used with the X-Symbol package.

    14

    15 Moreover, any single symbol (or ASCII character) may be prefixed by

    16 \verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as

    17 \verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and

    18 all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,,

    19 such as \verb,\<^bold>\<alpha>, for \isa{\isactrlbold{\isasymalpha}}.  Note

    20 that super- and subscripts may \emph{not} be combined with bold style.

    21

    22 Further details of Isabelle document preparation are covered in

    23 chapter~\ref{ch:present}.

    24

    25 \begin{center}

    26   \begin{isabellebody}

    27     \input{syms}

    28   \end{isabellebody}

    29 \end{center}

    30

    31 %%% Local Variables:

    32 %%% mode: latex

    33 %%% TeX-master: "system"

    34 %%% End: