# 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}