# HG changeset patch
# User wenzelm
# Date 971632259 -7200
# Node ID 7171f8ace3c1e42f3df3595f236d91c406ffc8c2
# Parent  2a726de6e12426c07e71327f8748cd27d9e73b30
more elements;

diff -r 2a726de6e124 -r 7171f8ace3c1 doc-src/isar.sty
--- a/doc-src/isar.sty	Sun Oct 15 19:50:35 2000 +0200
+++ b/doc-src/isar.sty	Sun Oct 15 19:50:59 2000 +0200
@@ -43,6 +43,7 @@
 \newcommand{\PROOFNAME}{\isarkeyword{proof}}
 \newcommand{\QEDNAME}{\isarkeyword{qed}}
 \newcommand{\BYNAME}{\isarkeyword{by}}
+\newcommand{\APPLYNAME}{\isarkeyword{apply}}
 \newcommand{\ISNAME}{\isarkeyword{is}}
 \newcommand{\CONCLNAME}{\isarkeyword{concl}}
 \newcommand{\LETNAME}{\isarkeyword{let}}
@@ -57,6 +58,9 @@
 \newcommand{\TYPES}{\isarkeyword{types}}
 \newcommand{\CONSTS}{\isarkeyword{consts}}
 \newcommand{\DEFS}{\isarkeyword{defs}}
+\newcommand{\AXCLASS}{\isarkeyword{axclass}}
+\newcommand{\INSTANCE}{\isarkeyword{instance}}
+\newcommand{\DECLARE}{\isarkeyword{declare}}
 \newcommand{\TEXT}{\isarkeyword{text}}
 \newcommand{\TXT}{\isarkeyword{txt}}
 \newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
@@ -77,6 +81,8 @@
 \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
 \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
 \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
+\newcommand{\APPLY}[1]{\APPLYNAME\I@optmeth{#1}}
+\newcommand{\DONE}{\isarkeyword{done}}
 \newcommand{\DOT}{\isarkeyword{.}}
 \newcommand{\DDOT}{\isarkeyword{.\,.}}
 \newcommand{\DDDOT}{\dots}