doc-src/Ref/tactic.tex

 
 \subsection{Inserting premises and facts}\label{cut_facts_tac}
 \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
 \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

     eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
   are inserted: Isabelle cannot use assumptions that contain $\Imp$
   or~$\Forall$.  Sometimes the theorems are premises of a rule being
   derived, returned by~{\tt goal}; instead of calling this tactic, you
   could state the goal with an outermost meta-quantifier.
-
-\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
-  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$. 
 
 \end{ttdescription}
 
 
 \subsection{Composition: resolution without lifting}