THEN* 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

© 1988-99, Carnegie Mellon University.

TPS homepage