tactic ::= atomic_tactic | ( tactic ) | tactic Orelse tactic | Repeat tactic | Do num tactic | Info tactic | Try tactic | First [ tactic | ... | tactic ] | Solve [ tactic | ... | tactic ] | Abstract tactic | Abstract tactic using ident | tactic ; tactic | tactic ;[ tactic |
...|
tactic ]tactic_invocation ::= num : tactic . | tactic .
Figure 7.1: Invocation of tactics and tacticals