# HG changeset patch
# User wenzelm
# Date 1327868769 -3600
# Node ID 1d215ebaaef1020e31fd8196a62885fbb1625ae1
# Parent  67139209b548d39ad74e2c16685816762a459035
removed obscure material;

diff -r 67139209b548 -r 1d215ebaaef1 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Sun Jan 29 21:04:39 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Sun Jan 29 21:26:09 2012 +0100
@@ -70,7 +70,6 @@
 \index{theorems!of pure theory}
 \begin{ttbox} 
 asm_rl: thm 
-cut_rl: thm 
 \end{ttbox}
 \begin{ttdescription}
 \item[\tdx{asm_rl}] 
@@ -80,9 +79,6 @@
 assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
 \end{ttbox}
 
-\item[\tdx{cut_rl}] 
-is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
-assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}.
 \end{ttdescription}
 
 
@@ -109,7 +105,6 @@
 \index{flex-flex constraints}
 \begin{ttbox} 
 distinct_subgoals_tac : tactic
-prune_params_tac      : tactic
 flexflex_tac          : tactic
 \end{ttbox}
 \begin{ttdescription}
@@ -117,12 +112,6 @@
   proof state.  (These arise especially in ZF, where the subgoals are
   essentially type constraints.)
 
-\item[\ttindexbold{prune_params_tac}]  
-  removes unused parameters from all subgoals of the proof state.  It works
-  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
-  make the proof state more readable.  It is used with
-  \ttindex{rule_by_tactic} to simplify the resulting theorem.
-
 \item[\ttindexbold{flexflex_tac}]  
   removes all flex-flex pairs from the proof state by applying the trivial
   unifier.  This drastic step loses information, and should only be done as