added \ISS;
authorwenzelm
Thu, 21 Oct 1999 15:57:26 +0200
changeset 7894 2ccfea468b24
parent 7893 fef0738b62d7
child 7895 7c492d8bc8e3
added \ISS;
doc-src/isar.sty
--- 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}