doc-src/System/symbols.tex
 author wenzelm Wed Jun 09 18:51:02 2004 +0200 (2004-06-09) changeset 14894 d23f6b505e9a parent 12619 ddfe8083fef2 permissions -rw-r--r--
updated notes on sub-/superscripts;
     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}}; the alternative

    18 versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters

    19 and may be used within identifiers.  Sub- and superscripts that span a region

    20 of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and

    21 \verb,\<^bsup>,\dots\verb,\<^esup>,, respectively.  Furthermore, all ASCII

    22 characters and most other symbols may be printed in bold by prefixing

    23 \verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for

    24 \isa{\isactrlbold{\isasymalpha}}.  Note that \verb,\<^bold>, may \emph{not} be

    25 combined with sub- or superscripts for single symbols.

    26

    27 Further details of Isabelle document preparation are covered in

    28 chapter~\ref{ch:present}.

    29

    30 \begin{center}

    31   \begin{isabellebody}

    32     \input{syms}

    33   \end{isabellebody}

    34 \end{center}

    35

    36 %%% Local Variables:

    37 %%% mode: latex

    38 %%% TeX-master: "system"

    39 %%% End: