doc-src/isar.sty
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}