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;
     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; they are also supported by Proof~General when
    11 used together with the X-Symbol package.
    12 
    13 \begin{center}
    14   \input{syms}  
    15 \end{center}
    16 
    17 Any symbol (or plain ASCII character) may be prefixed by a control sequence
    18 \verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript.  E.g.\ 
    19 \verb,A\<^sup>\<star>, is presented in {\LaTeX} as
    20 \isa{A\isactrlsup{\isasymstar}}.  See also Chapter~\ref{ch:present} for more
    21 information on Isabelle document preparation and related issues.
    22 
    23 %%% Local Variables: 
    24 %%% mode: latex
    25 %%% TeX-master: "system"
    26 %%% End: