--- a/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jan 29 21:26:09 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jan 29 21:40:29 2012 +0100
@@ -412,6 +412,8 @@
text %mlref {*
\begin{mldecls}
@{index_ML rotate_tac: "int -> int -> tactic"} \\
+ @{index_ML distinct_subgoals_tac: tactic} \\
+ @{index_ML flexflex_tac: tactic} \\
\end{mldecls}
\begin{description}
@@ -420,6 +422,19 @@
@{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.
+ \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a
+ proof state. This is potentially inefficient.
+
+ \item @{ML flexflex_tac} removes all flex-flex pairs from the proof
+ state by applying the trivial unifier. This drastic step loses
+ information. It is already part of the Isar infrastructure for
+ facts resulting from goals, and rarely needs to be invoked manually.
+
+ Flex-flex constraints arise from difficult cases of higher-order
+ unification. To prevent this, use @{ML res_inst_tac} to instantiate
+ some variables in a rule. Normally flex-flex constraints can be
+ ignored; they often disappear as unknowns get instantiated.
+
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Sun Jan 29 21:26:09 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Sun Jan 29 21:40:29 2012 +0100
@@ -497,6 +497,8 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{rotate\_tac}\verb|rotate_tac: int -> int -> tactic| \\
+ \indexdef{}{ML}{distinct\_subgoals\_tac}\verb|distinct_subgoals_tac: tactic| \\
+ \indexdef{}{ML}{flexflex\_tac}\verb|flexflex_tac: tactic| \\
\end{mldecls}
\begin{description}
@@ -505,6 +507,19 @@
\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.
+ \item \verb|distinct_subgoals_tac| removes duplicate subgoals from a
+ proof state. This is potentially inefficient.
+
+ \item \verb|flexflex_tac| removes all flex-flex pairs from the proof
+ state by applying the trivial unifier. This drastic step loses
+ information. It is already part of the Isar infrastructure for
+ facts resulting from goals, and rarely needs to be invoked manually.
+
+ Flex-flex constraints arise from difficult cases of higher-order
+ unification. To prevent this, use \verb|res_inst_tac| to instantiate
+ some variables in a rule. Normally flex-flex constraints can be
+ ignored; they often disappear as unknowns get instantiated.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Ref/tactic.tex Sun Jan 29 21:26:09 2012 +0100
+++ b/doc-src/Ref/tactic.tex Sun Jan 29 21:40:29 2012 +0100
@@ -99,32 +99,6 @@
\end{ttdescription}
-\subsection{Tidying the proof state}
-\index{duplicate subgoals!removing}
-\index{parameters!removing unused}
-\index{flex-flex constraints}
-\begin{ttbox}
-distinct_subgoals_tac : tactic
-flexflex_tac : tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
- proof state. (These arise especially in ZF, where the subgoals are
- essentially type constraints.)
-
-\item[\ttindexbold{flexflex_tac}]
- removes all flex-flex pairs from the proof state by applying the trivial
- unifier. This drastic step loses information, and should only be done as
- the last step of a proof.
-
- Flex-flex constraints arise from difficult cases of higher-order
- unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
- some variables in a rule~({\S}\ref{res_inst_tac}). Normally flex-flex
- constraints can be ignored; they often disappear as unknowns get
- instantiated.
-\end{ttdescription}
-
-
\subsection{Composition: resolution without lifting}
\index{tactics!for composition}
\begin{ttbox}