# HG changeset patch
# User wenzelm
# Date 1327867479 -3600
# Node ID 67139209b548d39ad74e2c16685816762a459035
# Parent  48cf461535cf2595febe84a4f15e2b5130a43b4f
updated rotate_tac;

diff -r 48cf461535cf -r 67139209b548 doc-src/IsarImplementation/Thy/Tactic.thy
--- 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
diff -r 48cf461535cf -r 67139209b548 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Sun Jan 29 21:04:39 2012 +0100
@@ -476,6 +476,46 @@
 %
 \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%
diff -r 48cf461535cf -r 67139209b548 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sun Jan 29 21:04:39 2012 +0100
@@ -347,11 +347,10 @@
   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   \emph{suffix} of variables.
 
-  \item @{method rotate_tac}~@{text n} rotates the assumptions of a
-  goal by @{text n} positions: from right to left if @{text n} is
+  \item @{method rotate_tac}~@{text n} rotates the premises of a
+  subgoal by @{text n} positions: from right to left if @{text n} is
   positive, and from left to right if @{text n} is negative; the
-  default value is 1.  See also @{ML rotate_tac} in
-  \cite{isabelle-implementation}.
+  default value is 1.
 
   \item @{method tactic}~@{text "text"} produces a proof method from
   any ML text of type @{ML_type tactic}.  Apart from the usual ML
diff -r 48cf461535cf -r 67139209b548 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sun Jan 29 21:04:39 2012 +0100
@@ -549,11 +549,10 @@
   goal according to the list \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, which refers to the
   \emph{suffix} of variables.
 
-  \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{n} rotates the assumptions of a
-  goal by \isa{n} positions: from right to left if \isa{n} is
+  \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{n} rotates the premises of a
+  subgoal by \isa{n} positions: from right to left if \isa{n} is
   positive, and from left to right if \isa{n} is negative; the
-  default value is 1.  See also \verb|rotate_tac| in
-  \cite{isabelle-implementation}.
+  default value is 1.
 
   \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} produces a proof method from
   any ML text of type \verb|tactic|.  Apart from the usual ML
diff -r 48cf461535cf -r 67139209b548 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Fri Jan 27 21:56:29 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Sun Jan 29 21:04:39 2012 +0100
@@ -89,10 +89,8 @@
 \section{Obscure tactics}
 
 \subsection{Manipulating assumptions}
-\index{assumptions!rotating}
 \begin{ttbox} 
 thin_tac   : string -> int -> tactic
-rotate_tac : int -> int -> tactic
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{thin_tac} {\it formula} $i$]  
@@ -102,12 +100,6 @@
 assumption will be deleted.  Removing useless assumptions from a subgoal
 increases its readability and can make search tactics run faster.
 
-\item[\ttindexbold{rotate_tac} $n$ $i$]  
-\index{assumptions!rotating}
-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.  This is 
-sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 
-processes assumptions from left to right.
 \end{ttdescription}