# HG changeset patch
# User wenzelm
# Date 754234966 -3600
# Node ID c5e636ca657698cebda4cfea2408d4f34d39de2b
# Parent  919a03a587eb0b233ced29b1d9d12ddf9e9b3416
corrected some obvious errors;

diff -r 919a03a587eb -r c5e636ca6576 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Nov 25 14:32:54 1993 +0100
+++ b/doc-src/Ref/thm.tex	Thu Nov 25 14:42:46 1993 +0100
@@ -100,13 +100,13 @@
   does not matter if the $thm@i$ create new premises.  {\tt MRS} is useful
   for expressing proof trees.
 
-\item[\tt$thms1$ RLN $(i,thms2)$] \indexbold{*RLN} 
-for every $thm@1$ in $thms1$ and $thm@2$ in $thms2$, it resolves the
+\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN} 
+for every $thm@1$ in $thms@1$ and $thm@2$ in $thms@2$, it resolves the
 conclusion of $thm@1$ with the $i$th premise of~$thm@2$, accumulating the
 results.  It is useful for combining lists of theorems.
 
-\item[\tt$thms1$ RL $thms2$] \indexbold{*RL} 
-abbreviates \hbox{\tt$thms1$ RLN $(1,thms2)$}. 
+\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL} 
+abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}. 
 
 \item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL} 
 is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
@@ -372,7 +372,7 @@
 
 \item[\ttindexbold{implies_elim_list} $thm$ $thms$] 
 applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
-turn.  It maps the premises $[\phi@1,\ldots,\phi@n]\Imp\psi$ and
+turn.  It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
 $\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
 \end{description}
 
@@ -401,7 +401,7 @@
 \end{ttbox}
 \begin{description}
 \item[\ttindexbold{reflexive} $ct$] 
-makes the theorem \(ct=ct\). 
+makes the theorem \(ct\equiv ct\). 
 
 \item[\ttindexbold{symmetric} $thm$] 
 maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
@@ -587,7 +587,7 @@
 analogous to {\tt RS}\@.  
 
 For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
-that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg A)$, which is the
+that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P)$, which is the
 principle of contrapositives.  Then the result would be the
 derived rule $\neg(b=a)\Imp\neg(a=b)$.