# HG changeset patch
# User wenzelm
# Date 952555045 -3600
# Node ID def06c4418930172875b8b45b7fbdee837d7905f
# Parent  f5628700ab9a2b0d7de5c15b2e93aec249bb5e5a
added \CASE, \OBTAIN, \SORRY, \OOPS;
removed \SUFF;

diff -r f5628700ab9a -r def06c441893 doc-src/isar.sty
--- 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}}