doc-src/System/symbols.tex
author wenzelm
Sat May 17 13:54:30 2008 +0200 (2008-05-17)
changeset 26928 ca87aff1ad2d
parent 14894 d23f6b505e9a
permissions -rw-r--r--
structure Display: less pervasive operations;
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@14894
    17
\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}; the alternative
wenzelm@14894
    18
versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters
wenzelm@14894
    19
and may be used within identifiers.  Sub- and superscripts that span a region
wenzelm@14894
    20
of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and
wenzelm@14894
    21
\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively.  Furthermore, all ASCII
wenzelm@14894
    22
characters and most other symbols may be printed in bold by prefixing
wenzelm@14894
    23
\verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for
wenzelm@14894
    24
\isa{\isactrlbold{\isasymalpha}}.  Note that \verb,\<^bold>, may \emph{not} be
wenzelm@14894
    25
combined with sub- or superscripts for single symbols.
wenzelm@11573
    26
wenzelm@12619
    27
Further details of Isabelle document preparation are covered in
wenzelm@12619
    28
chapter~\ref{ch:present}.
wenzelm@11573
    29
wenzelm@10580
    30
\begin{center}
wenzelm@12465
    31
  \begin{isabellebody}
wenzelm@12465
    32
    \input{syms}  
wenzelm@12465
    33
  \end{isabellebody}
wenzelm@10580
    34
\end{center}
wenzelm@10580
    35
wenzelm@10580
    36
%%% Local Variables: 
wenzelm@10580
    37
%%% mode: latex
wenzelm@10580
    38
%%% TeX-master: "system"
wenzelm@10580
    39
%%% End: