# HG changeset patch # User wenzelm # Date 869144618 -7200 # Node ID c02cb15830def6762e636ec96c76a51274e5255f # Parent 23eae933c2d90f7f25ac0f84d5b8bd7149478c8a fixed EqI meta rule; diff -r 23eae933c2d9 -r c02cb15830de doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Thu Jul 17 12:44:58 1997 +0200 +++ b/doc-src/Ref/ref.ind Thu Jul 17 15:03:38 1997 +0200 @@ -246,7 +246,7 @@ \item exceptions \subitem printing of, 5 \item {\tt exit}, \bold{2} - \item {\tt extensional}, \bold{44} + \item {\tt extensional}, \bold{43} \indexspace @@ -278,7 +278,7 @@ \item {\tt forall_elim}, \bold{44} \item {\tt forall_elim_list}, \bold{44} \item {\tt forall_elim_var}, \bold{44} - \item {\tt forall_elim_vars}, \bold{45} + \item {\tt forall_elim_vars}, \bold{44} \item {\tt forall_intr}, \bold{44} \item {\tt forall_intr_frees}, \bold{44} \item {\tt forall_intr_list}, \bold{44} @@ -325,7 +325,7 @@ \item {\tt implies_elim}, \bold{43} \item {\tt implies_elim_list}, \bold{43} \item {\tt implies_intr}, \bold{42} - \item {\tt implies_intr_hyps}, \bold{43} + \item {\tt implies_intr_hyps}, \bold{42} \item {\tt implies_intr_list}, \bold{42} \item {\tt incr_boundvars}, \bold{58}, 92 \item {\tt indexname} ML type, 57, 67 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} \]