1.1 --- a/doc-src/Ref/tactic.tex	Thu Jun 05 13:16:12 1997 +0200
     1.2 +++ b/doc-src/Ref/tactic.tex	Thu Jun 05 13:19:27 1997 +0200
     1.3 @@ -385,13 +385,19 @@
     1.4  
     1.5  
     1.6  \subsection{Tidying the proof state}
     1.7 +\index{duplicate subgoals!removing}
     1.8  \index{parameters!removing unused}
     1.9  \index{flex-flex constraints}
    1.10  \begin{ttbox} 
    1.11 -prune_params_tac : tactic
    1.12 -flexflex_tac     : tactic
    1.13 +distinct_subgoals_tac : tactic
    1.14 +prune_params_tac      : tactic
    1.15 +flexflex_tac          : tactic
    1.16  \end{ttbox}
    1.17  \begin{ttdescription}
    1.18 +\item[\ttindexbold{distinct_subgoals_tac}]  
    1.19 +  removes duplicate subgoals from a proof state.  (These arise especially
    1.20 +  in \ZF{}, where the subgoals are essentially type constraints.)
    1.21 +
    1.22  \item[\ttindexbold{prune_params_tac}]  
    1.23    removes unused parameters from all subgoals of the proof state.  It works
    1.24    by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can