--- a/doc-src/Ref/tactic.tex Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/Ref/tactic.tex Sun Jan 29 21:04:39 2012 +0100
@@ -89,10 +89,8 @@
\section{Obscure tactics}
\subsection{Manipulating assumptions}
-\index{assumptions!rotating}
\begin{ttbox}
thin_tac : string -> int -> tactic
-rotate_tac : int -> int -> tactic
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{thin_tac} {\it formula} $i$]
@@ -102,12 +100,6 @@
assumption will be deleted. Removing useless assumptions from a subgoal
increases its readability and can make search tactics run faster.
-\item[\ttindexbold{rotate_tac} $n$ $i$]
-\index{assumptions!rotating}
-rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
-if $n$ is positive, and from left to right if $n$ is negative. This is
-sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which
-processes assumptions from left to right.
\end{ttdescription}