Basic Tacticals

T1 ORELSE T2

Try running T1. If it fails, run T2 instead.

Run T1, and then on all subgoals generated by T1, run T2.

Run T1, generating exactly n subgoals. Then run Ti on the ith subgoal (numbering subgoals from left to right.)

T ORELSE Id

Run T. Fail if T generates one or more subgoals.

Run T. Fail if T makes no progress. (For example, if T is Id.)

Repeat application of T on subgoals generated by previous tries, until no further progress made.

Repeat application of T exactly n times.

If e p evaluates to TRUE then run T1. Otherwise, run T2.