/[mojave]/metaprl/theories/tactic/top_tacticals.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/top_tacticals.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3583 by nogin, Wed Jul 11 23:58:51 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 366  Line 366 
366   * including all the hypothesis and the conclusion.  The @tt{onHypsT} applies the   * including all the hypothesis and the conclusion.  The @tt{onHypsT} applies the
367   * argument only to the hypotheses.}   * argument only to the hypotheses.}
368   *   *
369   * @item{@tactic[onAllClausesT], @tactic[onAllHypsT];   * @item{@tactic[onAllAssumT];
370   * The (@tt{onAllAssumT} @i{tac}) applies the argument tactic to all the assumptions.   * The (@tt{onAllAssumT} @i{tac}) applies the argument tactic to all the assumptions.
371    ,    ,
372   * including all the hypothesis and the conclusion.  The @tt{onHypsT} applies the   * including all the hypothesis and the conclusion.  The @tt{onHypsT} applies the
# Line 423  Line 423 
423   * the current goal, the @tt{removeHiddenLabelT} tactic assigns   * the current goal, the @tt{removeHiddenLabelT} tactic assigns
424   * the label ``main'', and the (@tt{keepingLabelT} $@i{tac}$) applies   * the label ``main'', and the (@tt{keepingLabelT} $@i{tac}$) applies
425   * the tactic $@i{tac}$ and assigns the label of the current goal   * the tactic $@i{tac}$ and assigns the label of the current goal
426   * to all the the remaining subgoals.  The ``@tt{Hidden}'' is of historical   * to all of the remaining subgoals.  The ``@tt{Hidden}'' is of historical
427   * significance only@; the labels are hidden only in the sense that they   * significance only@; the labels are hidden only in the sense that they
428   * have no logical significance.}   * have no logical significance.}
429   *   *

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26