1.1 --- a/doc-src/Ref/tactic.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Ref/tactic.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -422,9 +422,9 @@
     1.4  flexflex_tac          : tactic
     1.5  \end{ttbox}
     1.6  \begin{ttdescription}
     1.7 -\item[\ttindexbold{distinct_subgoals_tac}]  
     1.8 -  removes duplicate subgoals from a proof state.  (These arise especially
     1.9 -  in \ZF{}, where the subgoals are essentially type constraints.)
    1.10 +\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
    1.11 +  proof state.  (These arise especially in ZF, where the subgoals are
    1.12 +  essentially type constraints.)
    1.13  
    1.14  \item[\ttindexbold{prune_params_tac}]  
    1.15    removes unused parameters from all subgoals of the proof state.  It works