doc-src/Ref/substitution.tex

   structure Simplifier : SIMPLIFIER
   val dest_Trueprop    : term -> term
   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) *)
   val sym              : thm         (* a=b ==> b=a *)
   val thin_refl        : thm         (* [|x=x; P|] ==> P *)

 \item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to
   the \ML{} term that represents the implication $P\imp Q$.  For other terms,
   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}$.
 
 \item[\tdxbold{rev_mp}] should be the `reversed' implies elimination