1.1 --- a/doc-src/Ref/tactic.tex	Fri Feb 14 10:35:06 1997 +0100
     1.2 +++ b/doc-src/Ref/tactic.tex	Fri Feb 14 10:35:23 1997 +0100
     1.3 @@ -315,46 +315,6 @@
     1.4  
     1.5  \section{Obscure tactics}
     1.6  
     1.7 -\subsection{Rotating assumptions}
     1.8 -\index{assumptions!rotating}
     1.9 -\begin{ttbox} 
    1.10 -rotate_tac : int -> int -> tactic
    1.11 -\end{ttbox}
    1.12 -\begin{ttdescription}
    1.13 -\item[\ttindexbold{rotate_tac} $n$ $i$]  
    1.14 -rotates the assumptions of subgoal $i$ by $n$ positions: from right to left,
    1.15 -if $n$ is positive, and from left to right, if $n$ is negative. Sometimes
    1.16 -necessary in connection with \ttindex{asm_full_simp_tac}.
    1.17 -
    1.18 -\end{ttdescription}
    1.19 -
    1.20 -\subsection{Tidying the proof state}
    1.21 -\index{parameters!removing unused}
    1.22 -\index{flex-flex constraints}
    1.23 -\begin{ttbox} 
    1.24 -prune_params_tac : tactic
    1.25 -flexflex_tac     : tactic
    1.26 -\end{ttbox}
    1.27 -\begin{ttdescription}
    1.28 -\item[\ttindexbold{prune_params_tac}]  
    1.29 -  removes unused parameters from all subgoals of the proof state.  It works
    1.30 -  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
    1.31 -  make the proof state more readable.  It is used with
    1.32 -  \ttindex{rule_by_tactic} to simplify the resulting theorem.
    1.33 -
    1.34 -\item[\ttindexbold{flexflex_tac}]  
    1.35 -  removes all flex-flex pairs from the proof state by applying the trivial
    1.36 -  unifier.  This drastic step loses information, and should only be done as
    1.37 -  the last step of a proof.
    1.38 -
    1.39 -  Flex-flex constraints arise from difficult cases of higher-order
    1.40 -  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
    1.41 -  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
    1.42 -  constraints can be ignored; they often disappear as unknowns get
    1.43 -  instantiated.
    1.44 -\end{ttdescription}
    1.45 -
    1.46 -
    1.47  \subsection{Renaming parameters in a goal} \index{parameters!renaming}
    1.48  \begin{ttbox} 
    1.49  rename_tac        : string -> int -> tactic
    1.50 @@ -401,6 +361,56 @@
    1.51  \end{ttdescription}
    1.52  
    1.53  
    1.54 +\subsection{Manipulating assumptions}
    1.55 +\index{assumptions!rotating}
    1.56 +\begin{ttbox} 
    1.57 +thin_tac   : string -> int -> tactic
    1.58 +rotate_tac : int -> int -> tactic
    1.59 +\end{ttbox}
    1.60 +\begin{ttdescription}
    1.61 +\item[\ttindexbold{thin_tac} {\it formula} $i$]  
    1.62 +\index{assumptions!deleting}
    1.63 +deletes the specified assumption from subgoal $i$.  Often the assumption
    1.64 +can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
    1.65 +assumption will be deleted.  Removing useless assumptions from a subgoal
    1.66 +increases its readability and can make search tactics run faster.
    1.67 +
    1.68 +\item[\ttindexbold{rotate_tac} $n$ $i$]  
    1.69 +\index{assumptions!rotating}
    1.70 +rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
    1.71 +if $n$ is positive, and from left to right if $n$ is negative.  This is 
    1.72 +sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 
    1.73 +processes assumptions from left to right.
    1.74 +\end{ttdescription}
    1.75 +
    1.76 +
    1.77 +\subsection{Tidying the proof state}
    1.78 +\index{parameters!removing unused}
    1.79 +\index{flex-flex constraints}
    1.80 +\begin{ttbox} 
    1.81 +prune_params_tac : tactic
    1.82 +flexflex_tac     : tactic
    1.83 +\end{ttbox}
    1.84 +\begin{ttdescription}
    1.85 +\item[\ttindexbold{prune_params_tac}]  
    1.86 +  removes unused parameters from all subgoals of the proof state.  It works
    1.87 +  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
    1.88 +  make the proof state more readable.  It is used with
    1.89 +  \ttindex{rule_by_tactic} to simplify the resulting theorem.
    1.90 +
    1.91 +\item[\ttindexbold{flexflex_tac}]  
    1.92 +  removes all flex-flex pairs from the proof state by applying the trivial
    1.93 +  unifier.  This drastic step loses information, and should only be done as
    1.94 +  the last step of a proof.
    1.95 +
    1.96 +  Flex-flex constraints arise from difficult cases of higher-order
    1.97 +  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
    1.98 +  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
    1.99 +  constraints can be ignored; they often disappear as unknowns get
   1.100 +  instantiated.
   1.101 +\end{ttdescription}
   1.102 +
   1.103 +
   1.104  \subsection{Composition: resolution without lifting}
   1.105  \index{tactics!for composition}
   1.106  \begin{ttbox}