--- a/doc-src/Ref/tactic.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/tactic.tex Thu Feb 05 10:26:59 1998 +0100
@@ -475,7 +475,7 @@
proof state are never updated (see~\S\ref{match_tac}).
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
-returns the number of new subgoals that bi-resolution would yield for the
+returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
pair (if applied to a suitable subgoal). This is $n$ if the flag is
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
of premises of the rule. Elim-resolution yields one fewer subgoal than