# HG changeset patch # User wenzelm # Date 954421908 -7200 # Node ID 87cddace4432e69325d8c7a2a9ba8b23a2ad9aa4 # Parent 33e2bd53aec3c3e91e6dee646121e04764ac2407 added \MOREOVER, \ULTIMATELY; diff -r 33e2bd53aec3 -r 87cddace4432 doc-src/isar.sty --- a/doc-src/isar.sty Thu Mar 30 14:28:54 2000 +0200 +++ b/doc-src/isar.sty Thu Mar 30 15:11:48 2000 +0200 @@ -86,6 +86,8 @@ \newcommand{\CMT}[1]{\CMTNAME~\text{#1}} \newcommand{\ALSO}{\isarkeyword{also}} \newcommand{\FINALLY}{\isarkeyword{finally}} +\newcommand{\MOREOVER}{\isarkeyword{moreover}} +\newcommand{\ULTIMATELY}{\isarkeyword{ultimately}} \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3} \newcommand{\BG}{\isarkeyword{\{\{}} \newcommand{\EN}{\isarkeyword{\}\}}}