Label Sensitive Tacticals

IfLab lab T1 T2

If lab matches label of p, run T1. Otherwise, run T2.

T1 THENM T2 T1 THEN IfLab `main` T2 Id
  T1 THENA T2 T1 THEN IfLab `aux` T2 Id
  T1 THENW T2 T1 THEN IfLab `wf` T2 Id
  IfLabL [l1,T1; l2,T2; ... ;ln,Tn]

Run the first T i for which l i matches label of p

Run tactic T then do the following on each subgoal, scanning the subgoals from left to right. Match the subgoal's label against each li until a match succeeds. Then if the subgoal also has number label j, retrieve the jth tactic from Tsi and run that tactic on the subgoal. If the subgoal has no number label, then pop the first tactic off the Tsi list and run that tactic. If there are not sufficient tactics in the appropriate lists, THENLL fails. If there are too many, then the excess are ignored. If a subgoals label doesn't match any of the li then run the Id tactic.

Run the tactics T1 to Tn on successive main subgoals.

Repeat the tactic T on main subgoals.

Repeat the tactic T on main subgoals exactly i times.