# HG changeset patch
# User paulson
# Date 855912923 -3600
# Node ID 28232396b60eab506cf40657977c52e44be818c4
# Parent  a5b6a632768d6642f84b277658f55b6faa8e768f
Documented thin_tac

diff -r a5b6a632768d -r 28232396b60e doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Fri Feb 14 10:35:06 1997 +0100
+++ b/doc-src/Ref/tactic.tex	Fri Feb 14 10:35:23 1997 +0100
@@ -315,46 +315,6 @@
 
 \section{Obscure tactics}
 
-\subsection{Rotating assumptions}
-\index{assumptions!rotating}
-\begin{ttbox} 
-rotate_tac : int -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{rotate_tac} $n$ $i$]  
-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. Sometimes
-necessary in connection with \ttindex{asm_full_simp_tac}.
-
-\end{ttdescription}
-
-\subsection{Tidying the proof state}
-\index{parameters!removing unused}
-\index{flex-flex constraints}
-\begin{ttbox} 
-prune_params_tac : tactic
-flexflex_tac     : tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{prune_params_tac}]  
-  removes unused parameters from all subgoals of the proof state.  It works
-  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
-  make the proof state more readable.  It is used with
-  \ttindex{rule_by_tactic} to simplify the resulting theorem.
-
-\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{Renaming parameters in a goal} \index{parameters!renaming}
 \begin{ttbox} 
 rename_tac        : string -> int -> tactic
@@ -401,6 +361,56 @@
 \end{ttdescription}
 
 
+\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$]  
+\index{assumptions!deleting}
+deletes the specified assumption from subgoal $i$.  Often the assumption
+can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
+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}
+
+
+\subsection{Tidying the proof state}
+\index{parameters!removing unused}
+\index{flex-flex constraints}
+\begin{ttbox} 
+prune_params_tac : tactic
+flexflex_tac     : tactic
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{prune_params_tac}]  
+  removes unused parameters from all subgoals of the proof state.  It works
+  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
+  make the proof state more readable.  It is used with
+  \ttindex{rule_by_tactic} to simplify the resulting theorem.
+
+\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}