--- a/doc-src/Logics/Old_HOL.tex Wed May 03 12:09:05 1995 +0200
+++ b/doc-src/Logics/Old_HOL.tex Wed May 03 12:17:30 1995 +0200
@@ -1357,8 +1357,8 @@
\end{warn}
The reduction rules of the {\tt case}-construct are in {\tt cases}. All
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
-{\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em
- var i}\/}'' applies structural induction over variable {\em var} to
+{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em
+ var i}\/} applies structural induction over variable {\em var} to
subgoal {\em i}.