--- a/doc-src/Ref/tactic.tex Fri May 07 17:50:43 1999 +0200
+++ b/doc-src/Ref/tactic.tex Mon May 10 15:16:49 1999 +0200
@@ -571,7 +571,7 @@
Do not consider using the primitives discussed in this section unless you
really need to code tactics from scratch.
-\subsection{Operations on type {\tt tactic}}
+\subsection{Operations on tactics}
\index{tactics!primitives for coding} A tactic maps theorems to sequences of
theorems. The type constructor for sequences (lazy lists) is called
\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,