1.1 --- a/doc-src/Ref/tactic.tex	Fri Jul 28 18:05:25 1995 +0200
     1.2 +++ b/doc-src/Ref/tactic.tex	Fri Jul 28 18:05:50 1995 +0200
     1.3 @@ -294,6 +294,20 @@
     1.4  
     1.5  
     1.6  \section{Obscure tactics}
     1.7 +
     1.8 +\subsection{Rotating assumptions}
     1.9 +\index{assumptions!rotating}
    1.10 +\begin{ttbox} 
    1.11 +rotate_tac : int -> int -> tactic
    1.12 +\end{ttbox}
    1.13 +\begin{ttdescription}
    1.14 +\item[\ttindexbold{rotate_tac} $n$ $i$]  
    1.15 +rotates the assumptions of subgoal $i$ by $n$ positions: from right to left,
    1.16 +if $n$ is positive, and from left to right, if $n$ is negative. Sometimes
    1.17 +necessary in connection with \ttindex{asm_full_simp_tac}.
    1.18 +
    1.19 +\end{ttdescription}
    1.20 +
    1.21  \subsection{Tidying the proof state}
    1.22  \index{parameters!removing unused}
    1.23  \index{flex-flex constraints}