# HG changeset patch
# User wenzelm
# Date 940514246 -7200
# Node ID 2ccfea468b24d79b340aa7762d50e8499e696a56
# Parent  fef0738b62d7f303b73c80446f3dfe72e5c634f4
added \ISS;

diff -r fef0738b62d7 -r 2ccfea468b24 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}