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 immediately remove the effects of each invocation of completion that ``fails''.

The default for completion is reduce.