# HG changeset patch
# User paulson
# Date 865509567 -7200
# Node ID 80c979e0d42f02c87c3576c380b8b6c075ba017e
# Parent  0c4efa9eac29ec46704c84a4bc167073c4856fc9
Documented the new distinct_subgoals_tac

diff -r 0c4efa9eac29 -r 80c979e0d42f doc-src/Ref/tactic.tex
--- 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