tuned \DOT, \DDOT;
authorwenzelm
Wed Jan 10 20:19:56 2001 +0100 (2001-01-10)
changeset 1086012f45010ecb5
parent 10859 b88ce3ed3b1d
child 10861 f2ffa2d97533
tuned \DOT, \DDOT;
doc-src/isar.sty
     1.1 --- a/doc-src/isar.sty	Wed Jan 10 20:19:34 2001 +0100
     1.2 +++ b/doc-src/isar.sty	Wed Jan 10 20:19:56 2001 +0100
     1.3 @@ -85,8 +85,8 @@
     1.4  \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
     1.5  \newcommand{\APPLY}[1]{\APPLYNAME\I@optmeth{#1}}
     1.6  \newcommand{\DONE}{\isarkeyword{done}}
     1.7 -\newcommand{\DOT}{\isarkeyword{.}}
     1.8 -\newcommand{\DDOT}{\isarkeyword{.\,.}}
     1.9 +\newcommand{\DOT}{\textbf{.}}
    1.10 +\newcommand{\DDOT}{\textbf{.\,.}}
    1.11  \newcommand{\DDDOT}{\dots}
    1.12  \newcommand{\IS}[1]{(\ISNAME~#1)}
    1.13  \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}