author wenzelm Sun, 29 Jan 2012 21:04:39 +0100 changeset 46274 67139209b548 parent 46273 48cf461535cf child 46275 1d215ebaaef1
updated rotate_tac;
 doc-src/IsarImplementation/Thy/Tactic.thy file | annotate | diff | comparison | revisions doc-src/IsarImplementation/Thy/document/Tactic.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/Generic.thy file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/document/Generic.tex file | annotate | diff | comparison | revisions doc-src/Ref/tactic.tex file | annotate | diff | comparison | revisions
--- 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 @@
%
%
+\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%
+%
+%
+%
+\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}%
+%
+%
+%
\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
-  \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
-  \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}