# HG changeset patch
# User nipkow
# Date 806947550 -7200
# Node ID 7059356e18e07a139ce046174fdb4850e044adea
# Parent  653f33d8d79187f48efc1492122d4010017f8059
added rotate_tac

diff -r 653f33d8d791 -r 7059356e18e0 doc-src/Ref/tactic.tex
--- 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}