# HG changeset patch
# User wenzelm
# Date 1329333410 -3600
# Node ID e641f8a9f0b7582a26ab0e1893c81a76a1e855d1
# Parent  4a607979290de909cbe6fe80643517c53bdf995b
removed redundant cut_inst_tac -- already covered in implementation manual;

diff -r 4a607979290d -r e641f8a9f0b7 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Wed Feb 15 19:55:45 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Wed Feb 15 20:16:50 2012 +0100
@@ -8,7 +8,6 @@
 \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}
@@ -21,11 +20,6 @@
   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}