# HG changeset patch
# User lcp
# Date 773941090 -7200
# Node ID 8577bc1c4e1befaf0c8dfac1112d964b7fd72c78
# Parent  f1df7fc211a7e9970ac43b3ba0f9903ab3865d4a
documented subgoals_tac

diff -r f1df7fc211a7 -r 8577bc1c4e1b doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Mon Jul 11 16:47:20 1994 +0200
+++ b/doc-src/Ref/tactic.tex	Mon Jul 11 17:38:10 1994 +0200
@@ -244,6 +244,7 @@
 cut_facts_tac : thm list -> int -> tactic
 cut_inst_tac  : (string*string)list -> thm -> int -> tactic
 subgoal_tac   : string -> int -> tactic
+subgoal_tacs  : string list -> int -> tactic
 \end{ttbox}
 These tactics add assumptions to a given subgoal.
 \begin{ttdescription}
@@ -264,6 +265,10 @@
 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
 adds the {\it formula} as a 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}