updated notes on sub-/superscripts;
Wed, 09 Jun 2004 18:51:02 +0200
changeset 14894 d23f6b505e9a
parent 14893 55e83c32cdec
child 14895 b9cc12a91fd3
updated notes on sub-/superscripts;
--- 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