changeset 3524 | c02cb15830de |
parent 3485 | f27a30a18a17 |
child 3657 | 48b8efdd1b80 |
--- 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} \]