--- a/doc-src/Ref/substitution.tex Mon May 05 21:18:01 1997 +0200
+++ b/doc-src/Ref/substitution.tex Tue May 06 12:50:16 1997 +0200
@@ -21,8 +21,10 @@
\section{Substitution rules}
\index{substitution!rules}\index{*subst theorem}
Many logics include a substitution rule of the form
-$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
- \Var{P}(\Var{b}) \eqno(subst)$$
+$$
+\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
+\Var{P}(\Var{b}) \eqno(subst)
+$$
In backward proof, this may seem difficult to use: the conclusion
$\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt
eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
@@ -42,8 +44,10 @@
resolve_tac [eqth RS ssubst] \(i\){\it,}
\end{ttbox}
where \tdxbold{ssubst} is the `swapped' substitution rule
-$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
- \Var{P}(\Var{a}). \eqno(ssubst)$$
+$$
+\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
+\Var{P}(\Var{a}). \eqno(ssubst)
+$$
If \tdx{sym} denotes the symmetry rule
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just
\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt
@@ -57,7 +61,7 @@
eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.}
\end{ttbox}
-Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
+Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by
\begin{ttbox}
fun stac eqth = CHANGED o rtac (eqth RS ssubst);
\end{ttbox}