ACL2-PC::THEN

(macro) apply one instruction to current goal and another to new subgoals
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(then induct prove)

General Form: (then first-instruction &optional completion must-succeed-flg)

Run first-instruction, and then run completion (another instruction) on each subgoal created by first-instruction. If must-succeed-flg is supplied and not nil, then halt at the first ``failure'' and remove the effects of the invocation of completion that ``failed''.

The default for completion is reduce.