# HG changeset patch
# User wenzelm
# Date 1086799862 -7200
# Node ID d23f6b505e9a5f02da76663eb5276df208c120e8
# Parent  55e83c32cdecf7d3991fa557c1a5138a3c4ff13c
updated notes on sub-/superscripts;

diff -r 55e83c32cdec -r d23f6b505e9a doc-src/System/symbols.tex
--- a/doc-src/System/symbols.tex	Wed Jun 09 18:50:38 2004 +0200
+++ b/doc-src/System/symbols.tex	Wed Jun 09 18:51:02 2004 +0200
@@ -14,10 +14,15 @@
 
 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.
+\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}; the alternative
+versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters
+and may be used within identifiers.  Sub- and superscripts that span a region
+of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and
+\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively.  Furthermore, all ASCII
+characters and most other symbols may be printed in bold by prefixing
+\verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for
+\isa{\isactrlbold{\isasymalpha}}.  Note that \verb,\<^bold>, may \emph{not} be
+combined with sub- or superscripts for single symbols.
 
 Further details of Isabelle document preparation are covered in
 chapter~\ref{ch:present}.