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;
wenzelm@10580
     1
wenzelm@10580
     2
% $Id$
wenzelm@10580
     3
wenzelm@12464
     4
\chapter{Standard 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@12619
     8
identifier).  It is left to front-end tools how to present these symbols to
wenzelm@12619
     9
the user.  The collection of predefined standard symbols given below is
wenzelm@12619
    10
available by default for Isabelle document output, due to appropriate
wenzelm@12619
    11
definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the
wenzelm@12619
    12
\verb,isabellesym.sty, file.  Most of these symbols are displayed properly in
wenzelm@12619
    13
Proof~General if used with the X-Symbol package.
wenzelm@10580
    14
wenzelm@12619
    15
Moreover, any single symbol (or ASCII character) may be prefixed by
wenzelm@12619
    16
\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
wenzelm@12619
    17
\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
wenzelm@12619
    18
all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,,
wenzelm@12619
    19
such as \verb,\<^bold>\<alpha>, for \isa{\isactrlbold{\isasymalpha}}.  Note
wenzelm@12619
    20
that super- and subscripts may \emph{not} be combined with bold style.
wenzelm@11573
    21
wenzelm@12619
    22
Further details of Isabelle document preparation are covered in
wenzelm@12619
    23
chapter~\ref{ch:present}.
wenzelm@11573
    24
wenzelm@10580
    25
\begin{center}
wenzelm@12465
    26
  \begin{isabellebody}
wenzelm@12465
    27
    \input{syms}  
wenzelm@12465
    28
  \end{isabellebody}
wenzelm@10580
    29
\end{center}
wenzelm@10580
    30
wenzelm@10580
    31
%%% Local Variables: 
wenzelm@10580
    32
%%% mode: latex
wenzelm@10580
    33
%%% TeX-master: "system"
wenzelm@10580
    34
%%% End: