# 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}   \]