author paulson Fri, 14 Feb 1997 10:35:23 +0100 changeset 2612 28232396b60e parent 2611 a5b6a632768d child 2613 cc4eb23d37b3
Documented thin_tac
 doc-src/Ref/tactic.tex file | annotate | diff | comparison | revisions
--- 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}