wenzelm@10580: 
wenzelm@10580: % $Id$
wenzelm@10580: 
wenzelm@10580: \chapter{Isabelle symbols}\label{app:symbols}
wenzelm@10580: 
wenzelm@10580: Isabelle supports an infinite number of non-ASCII symbols, which are
wenzelm@10580: represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
wenzelm@10580: identifier).  It is left to front-end tools how these symbols are presented to
wenzelm@10580: the user.  The following predefined standard symbols are available by default
wenzelm@10580: for Isabelle document output; they are also supported by Proof~General when
wenzelm@10580: used together with the X-Symbol package.
wenzelm@10580: 
wenzelm@10580: \begin{center}
wenzelm@10580:   \input{syms}  
wenzelm@10580: \end{center}
wenzelm@10580: 
wenzelm@10580: Any symbol (or plain ASCII character) may be prefixed by a control sequence
wenzelm@10580: \verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript.  E.g.\ 
wenzelm@10580: \verb,A\<^sup>\<star>, is presented in {\LaTeX} as
wenzelm@10580: \isa{A\isactrlsup{\isasymstar}}.  See also Chapter~\ref{ch:present} for more
wenzelm@10580: information on Isabelle document preparation and related issues.
wenzelm@10580: 
wenzelm@10580: %%% Local Variables: 
wenzelm@10580: %%% mode: latex
wenzelm@10580: %%% TeX-master: "system"
wenzelm@10580: %%% End: