--- a/doc-src/Logics/FOL.tex Fri Nov 26 12:31:48 1993 +0100
+++ b/doc-src/Logics/FOL.tex Fri Nov 26 12:54:58 1993 +0100
@@ -650,7 +650,7 @@
\[ if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R) \]
suggests that the
$if$-introduction rule should be
-\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{P} & \infer*{R}{\neg P}} \]
+\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \]
The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
elimination rules for~$\disj$ and~$\conj$.
\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}