--- a/doc-src/Ref/tactic.tex Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/Ref/tactic.tex Fri Jan 27 21:29:37 2012 +0100
@@ -9,8 +9,6 @@
\begin{ttbox}
cut_facts_tac : thm list -> int -> tactic
cut_inst_tac : (string*string)list -> thm -> int -> tactic
-subgoal_tac : string -> int -> tactic
-subgoals_tac : string list -> int -> tactic
\end{ttbox}
These tactics add assumptions to a subgoal.
\begin{ttdescription}
@@ -28,13 +26,6 @@
described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a
new assumption to subgoal~$i$.
-\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
-adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
-{\it formula} as a new subgoal, $i+1$.
-
-\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
- uses {\tt subgoal_tac} to add the members of the list of {\it
- formulae} as assumptions to subgoal~$i$.
\end{ttdescription}
@@ -91,8 +82,7 @@
\item[\tdx{cut_rl}]
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
-assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
-and {\tt subgoal_tac}.
+assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}.
\end{ttdescription}