doc-src/System/symbols.tex
 author wenzelm Tue Dec 11 15:58:32 2001 +0100 (2001-12-11) changeset 12465 47f79ad602d9 parent 12464 f9d3c92eae4d child 12619 ddfe8083fef2 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 these symbols are presented to

     9 the user.  The following predefined standard symbols are available by default

    10 for Isabelle document output; most of these are also supported by

    11 Proof~General when used together with the X-Symbol package.

    12

    13 Any symbol (or plain ASCII character) may be prefixed by \verb,\<^sup>, for

    14 superscript and \verb,\<^sub>, for subscript; e.g.\ \verb,A\<^sup>\<star>, is

    15 presented in {\LaTeX} as \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and

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

    17 in \verb,\<^bold>\<alpha>, which is printed as

    18 \isa{\isactrlbold{\isasymalpha}}.  Note that super- and subscripts may

    19 \emph{not} be combined with bold style.

    20

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

    22 preparation.

    23

    24 \begin{center}

    25   \begin{isabellebody}

    26     \input{syms}

    27   \end{isabellebody}

    28 \end{center}

    29

    30 %%% Local Variables:

    31 %%% mode: latex

    32 %%% TeX-master: "system"

    33 %%% End: