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;
wenzelm@10580
     1
wenzelm@10580
     2
% $Id$
wenzelm@10580
     3
wenzelm@10580
     4
\chapter{Isabelle symbols}\label{app:symbols}
wenzelm@10580
     5
wenzelm@10580
     6
Isabelle supports an infinite number of non-ASCII symbols, which are
wenzelm@10580
     7
represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
wenzelm@10580
     8
identifier).  It is left to front-end tools how these symbols are presented to
wenzelm@10580
     9
the user.  The following predefined standard symbols are available by default
wenzelm@10974
    10
for Isabelle document output; most of these are also supported by
wenzelm@10974
    11
Proof~General when used together with the X-Symbol package.
wenzelm@10580
    12
wenzelm@11573
    13
Any symbol (or plain ASCII character) may be prefixed by \verb,\<^sup>, for
wenzelm@11573
    14
superscript and \verb,\<^sub>, for subscript; e.g.\ \verb,A\<^sup>\<star>, is
wenzelm@11573
    15
presented in {\LaTeX} as \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
wenzelm@11573
    16
all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,, as
wenzelm@11573
    17
in \verb,\<^bold>\<alpha>, which is printed as
wenzelm@11573
    18
\isa{\isactrlbold{\isasymalpha}}.  Note that super- and subscripts may
wenzelm@11573
    19
\emph{not} be combined with bold style.
wenzelm@11573
    20
wenzelm@11573
    21
See also Chapter~\ref{ch:present} for more details on Isabelle document
wenzelm@11573
    22
preparation.
wenzelm@11573
    23
wenzelm@10580
    24
\begin{center}
wenzelm@10580
    25
  \input{syms}  
wenzelm@10580
    26
\end{center}
wenzelm@10580
    27
wenzelm@10580
    28
%%% Local Variables: 
wenzelm@10580
    29
%%% mode: latex
wenzelm@10580
    30
%%% TeX-master: "system"
wenzelm@10580
    31
%%% End: