1.1 --- a/doc-src/isar.sty	Mon Mar 13 23:01:09 2000 +0100
     1.2 +++ b/doc-src/isar.sty	Tue Mar 14 11:27:38 2000 +0100
     1.3 @@ -89,5 +89,6 @@
     1.4  \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1\isarkeyword{where}~\I@optname{#2}~#3}
     1.5  \newcommand{\BG}{\isarkeyword{\{\{}}
     1.6  \newcommand{\EN}{\isarkeyword{\}\}}}
     1.7 +\newcommand{\NEXT}{\isarkeyword{next}}
     1.8  \newcommand{\SORRY}{\isarkeyword{sorry}}
     1.9  \newcommand{\OOPS}{\isarkeyword{oops}}