author | wenzelm |
Tue, 14 Mar 2000 11:27:38 +0100 | |
changeset 8446 | fb73f193e577 |
parent 8445 | 86e99f863932 |
child 8447 | 1181723cf835 |
doc-src/isar.sty | file | annotate | diff | comparison | revisions |
--- 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}}