diff -r b88ce3ed3b1d -r 12f45010ecb5 doc-src/isar.sty --- a/doc-src/isar.sty Wed Jan 10 20:19:34 2001 +0100 +++ b/doc-src/isar.sty Wed Jan 10 20:19:56 2001 +0100 @@ -85,8 +85,8 @@ \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}} \newcommand{\APPLY}[1]{\APPLYNAME\I@optmeth{#1}} \newcommand{\DONE}{\isarkeyword{done}} -\newcommand{\DOT}{\isarkeyword{.}} -\newcommand{\DDOT}{\isarkeyword{.\,.}} +\newcommand{\DOT}{\textbf{.}} +\newcommand{\DDOT}{\textbf{.\,.}} \newcommand{\DDDOT}{\dots} \newcommand{\IS}[1]{(\ISNAME~#1)} \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}