diff -r ab4dcb9285e0 -r 8258c26ae084 doc-src/Logics/FOL.tex
--- 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]}