THEN* : TACTICALTHEN* is a tactical.
(THEN* tactic1 tactic2) will first apply tactic1; if it fails
then failure is returned, otherwise tactic2 is applied to each resulting
goal. If tactic2 fails on any of these goals, then the new goals obtained
as a result of applying tactic1 are returned, otherwise the new goals
obtained as the result of applying both tactic1 and tactic2 are returned.
TPS documentation homepage