doc-src/isar.sty
changeset 7976 8005c92a85d7
parent 7972 b95d183ae476
child 8377 def06c441893
--- a/doc-src/isar.sty	Fri Oct 29 18:31:08 1999 +0200
+++ b/doc-src/isar.sty	Fri Oct 29 19:00:51 1999 +0200
@@ -70,7 +70,6 @@
 \newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
 \newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
 \newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
-\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
 \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
 \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
 \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
@@ -80,10 +79,11 @@
 \newcommand{\IS}[1]{(\ISNAME~#1)}
 \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
 \newcommand{\LET}[1]{\LETNAME~#1}
-\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
 \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{\BG}{\isarkeyword{\{\{}}
+\newcommand{\EN}{\isarkeyword{\}\}}}