--- 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 "&") {
--- 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"
--- 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