--- a/doc-src/Ref/tactic.tex Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/Ref/tactic.tex Sun Jan 29 22:00:10 2012 +0100
@@ -84,21 +84,6 @@
\section{Obscure tactics}
-\subsection{Manipulating assumptions}
-\begin{ttbox}
-thin_tac : string -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{thin_tac} {\it formula} $i$]
-\index{assumptions!deleting}
-deletes the specified assumption from subgoal $i$. Often the assumption
-can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
-assumption will be deleted. Removing useless assumptions from a subgoal
-increases its readability and can make search tactics run faster.
-
-\end{ttdescription}
-
-
\subsection{Composition: resolution without lifting}
\index{tactics!for composition}
\begin{ttbox}