added \NEXT;
authorwenzelm
Tue, 14 Mar 2000 11:27:38 +0100
changeset 8446 fb73f193e577
parent 8445 86e99f863932
child 8447 1181723cf835
added \NEXT;
doc-src/isar.sty
--- a/doc-src/isar.sty	Mon Mar 13 23:01:09 2000 +0100
+++ b/doc-src/isar.sty	Tue Mar 14 11:27:38 2000 +0100
@@ -89,5 +89,6 @@
 \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1\isarkeyword{where}~\I@optname{#2}~#3}
 \newcommand{\BG}{\isarkeyword{\{\{}}
 \newcommand{\EN}{\isarkeyword{\}\}}}
+\newcommand{\NEXT}{\isarkeyword{next}}
 \newcommand{\SORRY}{\isarkeyword{sorry}}
 \newcommand{\OOPS}{\isarkeyword{oops}}