--- a/doc-src/Ref/tctical.tex Wed Jan 25 21:14:00 2012 +0100
+++ b/doc-src/Ref/tctical.tex Wed Jan 25 22:01:15 2012 +0100
@@ -204,71 +204,6 @@
\end{ttdescription}
-
-\subsection{Scanning for a subgoal by number}
-\index{tacticals!scanning for subgoals}
-\begin{ttbox}
-ALLGOALS : (int -> tactic) -> tactic
-TRYALL : (int -> tactic) -> tactic
-SOMEGOAL : (int -> tactic) -> tactic
-FIRSTGOAL : (int -> tactic) -> tactic
-REPEAT_SOME : (int -> tactic) -> tactic
-REPEAT_FIRST : (int -> tactic) -> tactic
-trace_goalno_tac : (int -> tactic) -> int -> tactic
-\end{ttbox}
-These apply a tactic function of type {\tt int -> tactic} to all the
-subgoal numbers of a proof state, and join the resulting tactics using
-\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
-subgoals, or to one subgoal.
-
-Suppose that the original proof state has $n$ subgoals.
-
-\begin{ttdescription}
-\item[\ttindexbold{ALLGOALS} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
-
-It applies {\it tacf} to all the subgoals, counting downwards (to
-avoid problems when subgoals are added or deleted).
-
-\item[\ttindexbold{TRYALL} {\it tacf}]
-is equivalent to
-\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
-
-It attempts to apply {\it tacf} to all the subgoals. For instance,
-the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
-assumption.
-
-\item[\ttindexbold{SOMEGOAL} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
-
-It applies {\it tacf} to one subgoal, counting downwards. For instance,
-the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
-failing if this is impossible.
-
-\item[\ttindexbold{FIRSTGOAL} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
-
-It applies {\it tacf} to one subgoal, counting upwards.
-
-\item[\ttindexbold{REPEAT_SOME} {\it tacf}]
-applies {\it tacf} once or more to a subgoal, counting downwards.
-
-\item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
-applies {\it tacf} once or more to a subgoal, counting upwards.
-
-\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
-applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
-is non-empty, then it is returned, with the side-effect of printing {\tt
-Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
-sequence and prints nothing.
-
-It indicates that `the tactic worked for subgoal~$i$' and is mainly used
-with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
-\end{ttdescription}
-
\index{tacticals|)}