| changeset 8446 | fb73f193e577 |
| parent 8377 | def06c441893 |
| child 8504 | 242527763a16 |
--- 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}}