doc-src/isar.sty

 \newcommand{\TYPES}{\isarkeyword{types}}
 \newcommand{\CONSTS}{\isarkeyword{consts}}
 \newcommand{\DEFS}{\isarkeyword{defs}}
 \newcommand{\TEXT}{\isarkeyword{text}}
 \newcommand{\TXT}{\isarkeyword{txt}}
-\newcommand{\NOTE}[2]{\NOTENAME~#1=#2}
+\newcommand{\NOTE}[2]{\NOTENAME\ifthenelse{\equal{}{#1}}{}{~#1=}#2}
 \newcommand{\FROM}[1]{\FROMNAME~#1}
 \newcommand{\WITH}[1]{\WITHNAME~#1}
 \newcommand{\FIX}[1]{\FIXNAME~#1}
 \newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
 \newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}

 \newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
 \newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
 \newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
 \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
 \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
+\newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
 \newcommand{\DOT}{\isarkeyword{.}}
 \newcommand{\DDOT}{\isarkeyword{.\,.}}
 \newcommand{\DDDOT}{\dots}
 \newcommand{\IS}[1]{(\ISNAME~#1)}
 \newcommand{\LET}[1]{\LETNAME~#1}