updated notes on sub-/superscripts;
authorwenzelm
Wed Jun 09 18:51:02 2004 +0200 (2004-06-09)
changeset 14894d23f6b505e9a
parent 14893 55e83c32cdec
child 14895 b9cc12a91fd3
updated notes on sub-/superscripts;
doc-src/System/symbols.tex
     1.1 --- a/doc-src/System/symbols.tex	Wed Jun 09 18:50:38 2004 +0200
     1.2 +++ b/doc-src/System/symbols.tex	Wed Jun 09 18:51:02 2004 +0200
     1.3 @@ -14,10 +14,15 @@
     1.4  
     1.5  Moreover, any single symbol (or ASCII character) may be prefixed by
     1.6  \verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
     1.7 -\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}.  Most symbols (and
     1.8 -all ASCII characters) may be printed in bold by prefixing \verb,\<^bold>,,
     1.9 -such as \verb,\<^bold>\<alpha>, for \isa{\isactrlbold{\isasymalpha}}.  Note
    1.10 -that super- and subscripts may \emph{not} be combined with bold style.
    1.11 +\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}; the alternative
    1.12 +versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters
    1.13 +and may be used within identifiers.  Sub- and superscripts that span a region
    1.14 +of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and
    1.15 +\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively.  Furthermore, all ASCII
    1.16 +characters and most other symbols may be printed in bold by prefixing
    1.17 +\verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for
    1.18 +\isa{\isactrlbold{\isasymalpha}}.  Note that \verb,\<^bold>, may \emph{not} be
    1.19 +combined with sub- or superscripts for single symbols.
    1.20  
    1.21  Further details of Isabelle document preparation are covered in
    1.22  chapter~\ref{ch:present}.