summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Sat, 07 Feb 1998 14:37:48 +0100 | |

changeset 4607 | 6759ba6d3cc1 |

parent 4606 | 73227403d497 |

child 4608 | cdf16a9fb2ce |

Added reference to rotate_prems

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}