author wenzelm Sun, 29 Jan 2012 21:26:09 +0100 changeset 46275 1d215ebaaef1 parent 46274 67139209b548 child 46276 8f1f33faf24e
removed obscure material;
 doc-src/Ref/tactic.tex file | annotate | diff | comparison | revisions
--- 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