doc-src/IsarImplementation/Thy/document/Tactic.tex

 %
 \isadelimmlref
 %
 \endisadelimmlref
 %
+\isamarkupsubsection{Rearranging goal states%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In rare situations there is a need to rearrange goal states:
+  either the overall collection of subgoals, or the local structure of
+  a subgoal.  Various administrative tactics allow to operate on the
+  concrete presentation these conceptual sets of formulae.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{rotate\_tac}\verb|rotate_tac: int -> int -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|rotate_tac|~\isa{n\ i} rotates the premises of subgoal
+  \isa{i} by \isa{n} positions: from right to left if \isa{n} is
+  positive, and from left to right if \isa{n} is negative.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsection{Tacticals \label{sec:tacticals}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%