--- a/doc-src/Ref/tactic.tex Fri Jul 28 18:05:25 1995 +0200
+++ b/doc-src/Ref/tactic.tex Fri Jul 28 18:05:50 1995 +0200
@@ -294,6 +294,20 @@
\section{Obscure tactics}
+
+\subsection{Rotating assumptions}
+\index{assumptions!rotating}
+\begin{ttbox}
+rotate_tac : int -> int -> tactic
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{rotate_tac} $n$ $i$]
+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. Sometimes
+necessary in connection with \ttindex{asm_full_simp_tac}.
+
+\end{ttdescription}
+
\subsection{Tidying the proof state}
\index{parameters!removing unused}
\index{flex-flex constraints}