doc-src/System/symbols.tex
author wenzelm
Wed Sep 26 22:25:23 2001 +0200 (2001-09-26)
changeset 11573 4f85af77038f
parent 10974 f23a58cf12a4
child 12464 f9d3c92eae4d
permissions -rw-r--r--
bold symbols;
     1 
     2 % $Id$
     3 
     4 \chapter{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   \input{syms}  
    26 \end{center}
    27 
    28 %%% Local Variables: 
    29 %%% mode: latex
    30 %%% TeX-master: "system"
    31 %%% End: