Next: Case Splits and
Up: Tacticals
Previous: Label Sensitive Tacticals
AllHyps (T : int -> tactic)
-
- Try running T on each hypothesis starting with the end of the
hypothesis list and working backwards. If T succeeds on some
hypothesis, then AllHyps only continues on subgoals created by T
that are labelled main.
All (T : int -> tactic)
-
- Similar to AllHyps, except that also tries applying T to
conclusion after trying to apply it to hypotheses.
On [c1;...;cn] (T : int -> tactic) 
T c1 THENM ... THENM T cn
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996