changeset 7894 | 2ccfea468b24 |
parent 7511 | 85cf7fa5b138 |
child 7896 | 36865f14e5ce |
--- a/doc-src/isar.sty Wed Oct 20 15:53:22 1999 +0200 +++ b/doc-src/isar.sty Thu Oct 21 15:57:26 1999 +0200 @@ -82,6 +82,7 @@ \newcommand{\DDOT}{\isarkeyword{.\,.}} \newcommand{\DDDOT}{\dots} \newcommand{\IS}[1]{(\ISNAME~#1)} +\newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)} \newcommand{\LET}[1]{\LETNAME~#1} \newcommand{\LETT}[1]{\LETNAME~#1\dt\;} \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}