doc-src/Ref/tactic.tex

   instantiates the {\it thm} with the instantiations {\it insts}, as
   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 a assumption to subgoal~$i$, and inserts the same
+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$.