# HG changeset patch
# User wenzelm
# Date 1001535923 -7200
# Node ID 4f85af77038ff96fa573767a74735495b56fbecb
# Parent  93da54c8a687cda49ff88b2d29fa6c6769b71a8b
bold symbols;

diff -r 93da54c8a687 -r 4f85af77038f doc-src/System/showsymbols
--- a/doc-src/System/showsymbols	Wed Sep 26 22:24:55 2001 +0200
+++ b/doc-src/System/showsymbols	Wed Sep 26 22:25:23 2001 +0200
@@ -9,6 +9,7 @@
 while (<ARGV>) {
     if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
        print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
+#       print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
 #       print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
 #       print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
         if ("$eol" eq "&") {
diff -r 93da54c8a687 -r 4f85af77038f doc-src/System/symbols.tex
--- a/doc-src/System/symbols.tex	Wed Sep 26 22:24:55 2001 +0200
+++ b/doc-src/System/symbols.tex	Wed Sep 26 22:25:23 2001 +0200
@@ -10,16 +10,21 @@
 for Isabelle document output; most of these are also supported by
 Proof~General when used together 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.
+
+See also Chapter~\ref{ch:present} for more details on Isabelle document
+preparation.
+
 \begin{center}
   \input{syms}  
 \end{center}
 
-Any symbol (or plain ASCII character) may be prefixed by a control sequence
-\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript.  E.g.\ 
-\verb,A\<^sup>\<star>, is presented in {\LaTeX} as
-\isa{A\isactrlsup{\isasymstar}}.  See also Chapter~\ref{ch:present} for more
-information on Isabelle document preparation and related issues.
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "system"
diff -r 93da54c8a687 -r 4f85af77038f lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Sep 26 22:24:55 2001 +0200
+++ b/lib/texinputs/isabelle.sty	Wed Sep 26 22:25:23 2001 +0200
@@ -24,6 +24,7 @@
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip