# HG changeset patch
# User paulson
# Date 886858668 -3600
# Node ID 6759ba6d3cc1d4031eaadd38c1d970ff90a8c7ca
# Parent  73227403d497aafacee25a954c40279ca53e5ece
Added reference to rotate_prems

diff -r 73227403d497 -r 6759ba6d3cc1 doc-src/Ref/tactic.tex
--- 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
diff -r 73227403d497 -r 6759ba6d3cc1 doc-src/Ref/thm.tex
--- 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}