--- 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
--- 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%
--- 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
--- 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
--- 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}