--- a/doc-src/Ref/tactic.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Ref/tactic.tex Mon Aug 28 13:52:38 2000 +0200
@@ -422,9 +422,9 @@
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{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