1.1 --- a/doc-src/isar.sty	Mon Aug 23 15:24:00 1999 +0200
     1.2 +++ b/doc-src/isar.sty	Mon Aug 23 15:27:27 1999 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  \newcommand{\DEFS}{\isarkeyword{defs}}
     1.5  \newcommand{\TEXT}{\isarkeyword{text}}
     1.6  \newcommand{\TXT}{\isarkeyword{txt}}
     1.7 -\newcommand{\NOTE}[2]{\NOTENAME\ifthenelse{\equal{}{#1}}{}{~#1=}#2}
     1.8 +\newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
     1.9  \newcommand{\FROM}[1]{\FROMNAME~#1}
    1.10  \newcommand{\WITH}[1]{\WITHNAME~#1}
    1.11  \newcommand{\FIX}[1]{\FIXNAME~#1}