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: