# HG changeset patch
# User lcp
# Date 799496250 -7200
# Node ID 46a7b619e62e2bcc7a90aa8003064e95bd348876
# Parent  504dad4d78430109c1928ee840c7cb96841deafb
trivial change

diff -r 504dad4d7843 -r 46a7b619e62e doc-src/Logics/Old_HOL.tex
--- 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}.