--- a/doc-src/isar.sty Wed Mar 08 18:08:08 2000 +0100
+++ b/doc-src/isar.sty Wed Mar 08 23:37:25 2000 +0100
@@ -33,6 +33,7 @@
\newcommand{\FIXNAME}{\isarkeyword{fix}}
\newcommand{\ASSUMENAME}{\isarkeyword{assume}}
\newcommand{\PRESUMENAME}{\isarkeyword{presume}}
+\newcommand{\CASENAME}{\isarkeyword{case}}
\newcommand{\HAVENAME}{\isarkeyword{have}}
\newcommand{\SHOWNAME}{\isarkeyword{show}}
\newcommand{\HENCENAME}{\isarkeyword{hence}}
@@ -44,7 +45,7 @@
\newcommand{\CONCLNAME}{\isarkeyword{concl}}
\newcommand{\LETNAME}{\isarkeyword{let}}
\newcommand{\DEFNAME}{\isarkeyword{def}}
-\newcommand{\SUFFNAME}{\isarkeyword{suffient}}
+\newcommand{\OBTAINNAME}{\isarkeyword{obtain}}
\newcommand{\CMTNAME}{\isarkeyword{-{}-}}
\newcommand{\THEORY}{\isarkeyword{theory}}
@@ -62,6 +63,7 @@
\newcommand{\FIX}[1]{\FIXNAME~#1}
\newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
\newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}
+\newcommand{\CASE}[1]{\CASENAME~#1}
\newcommand{\THEN}{\isarkeyword{then}}
\newcommand{\HAVE}[2]{\isarkeyword{have}\I@optname{#1}~#2}
\newcommand{\SHOW}[2]{\isarkeyword{show}\I@optname{#1}~#2}
@@ -80,10 +82,12 @@
\newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
\newcommand{\LET}[1]{\LETNAME~#1}
\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
-\newcommand{\SUFF}[1]{\SUFFNAME~#1}
\newcommand{\ATT}[1]{\ap [#1]}
\newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
\newcommand{\ALSO}{\isarkeyword{also}}
\newcommand{\FINALLY}{\isarkeyword{finally}}
+\newcommand{\OBTAIN}[3]{\OBTAINNAME~#1\isarkeyword{where}~\I@optname{#2}~#3}
\newcommand{\BG}{\isarkeyword{\{\{}}
\newcommand{\EN}{\isarkeyword{\}\}}}
+\newcommand{\SORRY}{\isarkeyword{sorry}}
+\newcommand{\OOPS}{\isarkeyword{oops}}