doc-src/Ref/substitution.tex

--- a/doc-src/Ref/substitution.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/substitution.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -3,19 +3,18 @@
 \index{tactics!substitution|(}\index{equality|(}
 
 Replacing equals by equals is a basic form of reasoning.  Isabelle supports
-several kinds of equality reasoning.  {\bf Substitution} means to replace
+several kinds of equality reasoning.  {\bf Substitution} means replacing
 free occurrences of~$t$ by~$u$ in a subgoal.  This is easily done, given an
-equality $t=u$, provided the logic possesses the appropriate rule ---
-unless you want to substitute even in the assumptions.  The tactic
-{\tt hyp_subst_tac} performs substitution in the assumptions, but it
-works via object-level implication, and therefore must be specially set up
-for each suitable object-logic.
+equality $t=u$, provided the logic possesses the appropriate rule.  The
+tactic {\tt hyp_subst_tac} performs substitution even in the assumptions.
+But it works via object-level implication, and therefore must be specially
+set up for each suitable object-logic.
 
 Substitution should not be confused with object-level {\bf rewriting}.
 Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
 corresponding instances of~$u$, and continues until it reaches a normal
 form.  Substitution handles `one-off' replacements by particular
-equalities, while rewriting handles general equalities.
+equalities while rewriting handles general equations.
 Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
 
 
@@ -35,12 +34,12 @@
 the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in
 subgoal~$i$, use
 \begin{ttbox} 
-resolve_tac [eqth RS subst] \(i\) {\it.}
+resolve_tac [eqth RS subst] \(i\){\it.}
 \end{ttbox}
 To replace $t$ by~$u$ in
 subgoal~$i$, use
 \begin{ttbox} 
-resolve_tac [eqth RS ssubst] \(i\) {\it,}
+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 
@@ -55,7 +54,7 @@
 Elim-resolution is well-behaved with assumptions of the form $t=u$.
 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
 \begin{ttbox} 
-eresolve_tac [subst] \(i\)    {\it or}    eresolve_tac [ssubst] \(i\) {\it.}
+eresolve_tac [subst] \(i\)    {\rm or}    eresolve_tac [ssubst] \(i\){\it.}
 \end{ttbox}
 
 
@@ -93,7 +92,7 @@
 contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
 in the subgoal!
 
-Replacing a free variable causes similar problems if they appear in the
+Substitution for free variables is also unhelpful if they appear in the
 premises of a rule being derived --- the substitution affects object-level
 assumptions, not meta-level assumptions.  For instance, replacing~$a$
 by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, use
@@ -153,7 +152,7 @@
 Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
-to hide the types.
+for the types.
 
 Here is how {\tt hyp_subst_tac} works.  Given a subgoal of the form
 \[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \] it locates a suitable