diff -r 23eae933c2d9 -r c02cb15830de doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Thu Jul 17 12:44:58 1997 +0200
+++ b/doc-src/Ref/thm.tex	Thu Jul 17 15:03:38 1997 +0200
@@ -356,8 +356,8 @@
 
 \index{meta-equality}
 Equality of truth values means logical equivalence:
-\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} &
-                                       \infer*{\phi}{[\psi]}}  
+\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi &
+                                       \psi\Imp\phi}
    \qquad
    \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]