# 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)$.