# HG changeset patch
# User wenzelm
# Date 965422474 -7200
# Node ID 5721615da108beb69c20ac8ac4fa546c9494c1da
# Parent  232b09dba0fe808c343735479e1938b786389f65
added rev_eq_reflection;

diff -r 232b09dba0fe -r 5721615da108 doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Fri Aug 04 22:53:44 2000 +0200
+++ b/doc-src/Ref/substitution.tex	Fri Aug 04 22:54:34 2000 +0200
@@ -129,6 +129,7 @@
   val dest_eq          : term -> term*term*typ
   val dest_imp         : term -> term*term
   val eq_reflection    : thm         (* a=b ==> a==b *)
+  val rev_eq_reflection: thm         (* a==b ==> a=b *)
   val imp_intr         : thm         (*(P ==> Q) ==> P-->Q *)
   val rev_mp           : thm         (* [| P;  P-->Q |] ==> Q *)
   val subst            : thm         (* [| a=b;  P(a) |] ==> P(b) *)
@@ -154,7 +155,9 @@
   it should raise an exception.
 
 \item[\tdxbold{eq_reflection}] is the theorem discussed
-  in~\S\ref{sec:setting-up-simp}. 
+  in~\S\ref{sec:setting-up-simp}.
+  
+\item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.
 
 \item[\tdxbold{imp_intr}] should be the implies introduction
 rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.