doc-src/Ref/tactic.tex

 \index{tactics!for inserting facts}\index{assumptions!inserting}
 \begin{ttbox} 
 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
+subgoals_tac  : string list -> int -> tactic
 \end{ttbox}
 These tactics add assumptions to a subgoal.
 \begin{ttdescription}
 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
   adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have