--- a/doc-src/Ref/tactic.tex Thu Jun 05 13:16:12 1997 +0200
+++ b/doc-src/Ref/tactic.tex Thu Jun 05 13:19:27 1997 +0200
@@ -385,13 +385,19 @@
\subsection{Tidying the proof state}
+\index{duplicate subgoals!removing}
\index{parameters!removing unused}
\index{flex-flex constraints}
\begin{ttbox}
-prune_params_tac : tactic
-flexflex_tac : tactic
+distinct_subgoals_tac : tactic
+prune_params_tac : tactic
+flexflex_tac : tactic
\end{ttbox}
\begin{ttdescription}
+\item[\ttindexbold{distinct_subgoals_tac}]
+ removes duplicate subgoals from a proof state. (These arise especially
+ in \ZF{}, where the subgoals are essentially type constraints.)
+
\item[\ttindexbold{prune_params_tac}]
removes unused parameters from all subgoals of the proof state. It works
by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can