# HG changeset patch
# User wenzelm
# Date 1010004885 -3600
# Node ID ddfe8083fef2a9606979fff8198288ab0768a170
# Parent  43a97a2155d027d799096c596257107d58f5145e
tuned;

diff -r 43a97a2155d0 -r ddfe8083fef2 doc-src/System/symbols.tex
--- a/doc-src/System/symbols.tex	Wed Jan 02 21:53:50 2002 +0100
+++ b/doc-src/System/symbols.tex	Wed Jan 02 21:54:45 2002 +0100
@@ -5,21 +5,22 @@
 
 Isabelle supports an infinite number of non-ASCII symbols, which are
 represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
-identifier).  It is left to front-end tools how these symbols are presented to
-the user.  The following predefined standard symbols are available by default
-for Isabelle document output; most of these are also supported by
-Proof~General when used together with the X-Symbol package.
+identifier).  It is left to front-end tools how to present these symbols to
+the user.  The collection of predefined standard symbols given below is
+available by default for Isabelle document output, due to appropriate
+definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the
+\verb,isabellesym.sty, file.  Most of these symbols are displayed properly in
+Proof~General if used with the X-Symbol package.
 
-Any symbol (or plain ASCII character) may be prefixed by \verb,\<^sup>, for
-superscript and \verb,\<^sub>, for subscript; e.g.\ \verb,A\<^sup>\<star>, is
-presented in {\LaTeX} as \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
-all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,, as
-in \verb,\<^bold>\<alpha>, which is printed as
-\isa{\isactrlbold{\isasymalpha}}.  Note that super- and subscripts may
-\emph{not} be combined with bold style.
+Moreover, any single symbol (or ASCII character) may be prefixed by
+\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
+\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
+all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,,
+such as \verb,\<^bold>\<alpha>, for \isa{\isactrlbold{\isasymalpha}}.  Note
+that super- and subscripts may \emph{not} be combined with bold style.
 
-See also Chapter~\ref{ch:present} for more details on Isabelle document
-preparation.
+Further details of Isabelle document preparation are covered in
+chapter~\ref{ch:present}.
 
 \begin{center}
   \begin{isabellebody}