author paulson Sat, 07 Feb 1998 14:37:48 +0100 changeset 4607 6759ba6d3cc1 parent 4606 73227403d497 child 4608 cdf16a9fb2ce
 doc-src/Ref/tactic.tex file | annotate | diff | comparison | revisions doc-src/Ref/thm.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/tactic.tex	Fri Feb 06 18:55:57 1998 +0100
+++ b/doc-src/Ref/tactic.tex	Sat Feb 07 14:37:48 1998 +0100
@@ -45,9 +45,10 @@
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
\index{elim-resolution}
performs elim-resolution with the rules, which should normally be
-  elimination rules.  It resolves with a rule, solves its first premise by
-  assumption, and finally {\em deletes\/} that assumption from any new
-  subgoals.
+  elimination rules.  It resolves with a rule, proves its first premise by
+  assumption, and finally \emph{deletes} that assumption from any new
+  subgoals.  (To rotate a rule's premises,
+  see \texttt{rotate_prems} in~\S\ref{MiscellaneousForwardRules}.)

\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
\index{forward proof}\index{destruct-resolution}
@@ -73,7 +74,7 @@

\item[\ttindexbold{eq_assume_tac}]
is like {\tt assume_tac} but does not use unification.  It succeeds (with a
-{\em unique\/} next state) if one of the assumptions is identical to the
+\emph{unique} next state) if one of the assumptions is identical to the
subgoal's conclusion.  Since it does not instantiate variables, it cannot
make other subgoals unprovable.  It is intended to be called from proof
strategies, not interactively.
@@ -116,7 +117,7 @@
induction, which cause difficulties for higher-order unification.  The
tactics accept explicit instantiations for unknowns in the rule ---
typically, in the rule's conclusion.  Each instantiation is a pair
-{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
+{\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading
question mark!
\begin{itemize}
\item If $v$ is the type unknown {\tt'a}, then
--- a/doc-src/Ref/thm.tex	Fri Feb 06 18:55:57 1998 +0100
+++ b/doc-src/Ref/thm.tex	Sat Feb 07 14:37:48 1998 +0100
@@ -186,6 +186,7 @@
zero_var_indexes :           thm -> thm
make_elim        :           thm -> thm
rule_by_tactic   : tactic -> thm -> thm
+rotate_prems     :    int -> thm -> thm
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
@@ -211,6 +212,13 @@
with contradictory assumptions (because of the instantiation).  The
tactic proves those subgoals and does whatever else it can, and returns
whatever is left.
+
+\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
+  the left by~$k$ positions.  It requires $0\leq k\leq n$, where $n$ is the
+  number of premises; the rotation has no effect if $k$ is at either extreme.
+  Used with \texttt{eresolve_tac}\index{*eresolve_tac!on other than first
+    premise}, it gives the effect of applying the tactic to some other premise
+  of $thm$ than the first.
\end{ttdescription}