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: