Correction to page 16; thanks to Markus W.
authorlcp
Fri Nov 26 12:54:58 1993 +0100 (1993-11-26)
changeset 1578258c26ae084
parent 156 ab4dcb9285e0
child 158 c2fcb6c07689
Correction to page 16; thanks to Markus W.
doc-src/Logics/FOL.tex
     1.1 --- a/doc-src/Logics/FOL.tex	Fri Nov 26 12:31:48 1993 +0100
     1.2 +++ b/doc-src/Logics/FOL.tex	Fri Nov 26 12:54:58 1993 +0100
     1.3 @@ -650,7 +650,7 @@
     1.4  \[ if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R) \]
     1.5  suggests that the
     1.6  $if$-introduction rule should be
     1.7 -\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{P}  &  \infer*{R}{\neg P}} \]
     1.8 +\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]}  &  \infer*{R}{[\neg P]}} \]
     1.9  The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
    1.10  elimination rules for~$\disj$ and~$\conj$.
    1.11  \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}