--- a/doc-src/IsarImplementation/Thy/Tactic.thy Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jan 29 21:04:39 2012 +0100
@@ -402,6 +402,27 @@
*}
+subsection {* Rearranging goal states *}
+
+text {* 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. *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML rotate_tac: "int -> int -> tactic"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal
+ @{text i} by @{text n} positions: from right to left if @{text n} is
+ positive, and from left to right if @{text n} is negative.
+
+ \end{description}
+*}
+
section {* Tacticals \label{sec:tacticals} *}
text {* A \emph{tactical} is a functional combinator for building up