# HG changeset patch
# User wenzelm
# Date 953029658 -3600
# Node ID fb73f193e57774126218d450b81108abf4faee22
# Parent  86e99f86393201d5bf1a770fd96c7c88fb75803d
added \NEXT;

diff -r 86e99f863932 -r fb73f193e577 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}}