doc-src/System/symbols.tex
author wenzelm
Mon Dec 04 23:16:25 2000 +0100 (2000-12-04)
changeset 10580 930ac2bfa637
child 10974 f23a58cf12a4
permissions -rw-r--r--
include table of Isabelle standard 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@10580
    10
for Isabelle document output; they are also supported by Proof~General when
wenzelm@10580
    11
used together with the X-Symbol package.
wenzelm@10580
    12
wenzelm@10580
    13
\begin{center}
wenzelm@10580
    14
  \input{syms}  
wenzelm@10580
    15
\end{center}
wenzelm@10580
    16
wenzelm@10580
    17
Any symbol (or plain ASCII character) may be prefixed by a control sequence
wenzelm@10580
    18
\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript.  E.g.\ 
wenzelm@10580
    19
\verb,A\<^sup>\<star>, is presented in {\LaTeX} as
wenzelm@10580
    20
\isa{A\isactrlsup{\isasymstar}}.  See also Chapter~\ref{ch:present} for more
wenzelm@10580
    21
information on Isabelle document preparation and related issues.
wenzelm@10580
    22
wenzelm@10580
    23
%%% Local Variables: 
wenzelm@10580
    24
%%% mode: latex
wenzelm@10580
    25
%%% TeX-master: "system"
wenzelm@10580
    26
%%% End: