# 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}$.