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 |

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 |
* |
* |