# HG changeset patch
# User wenzelm
# Date 1327869629 -3600
# Node ID 8f1f33faf24e9ee2b632f5662875edfd2ca75b8d
# Parent  1d215ebaaef1020e31fd8196a62885fbb1625ae1
updated distinct_subgoals_tac, flexflex_tac;

diff -r 1d215ebaaef1 -r 8f1f33faf24e doc-src/IsarImplementation/Thy/Tactic.thy
--- 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}
 *}
 
diff -r 1d215ebaaef1 -r 8f1f33faf24e doc-src/IsarImplementation/Thy/document/Tactic.tex
--- 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%
diff -r 1d215ebaaef1 -r 8f1f33faf24e doc-src/Ref/tactic.tex
--- 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}