ACL2-PC::WRAP

(atomic macro) execute the indicated instructions and combine all the new goals
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(wrap induct) ; induct, then replace first new goal by the conjunction of all
              ; the new goals, and drop all new goals after the first

General Form: (wrap &rest instrs)

First the instructions in instrs are executed, as in do-all. If this ``fails'' then no additional action is taken. Otherwise, the current goal after execution of instrs is conjoined with all ``new'' goals, in the sense that their names are not among the names of goals at the time instrs was begun. This conjunction becomes the new current goal and those ``new'' goals are dropped.

See the code for the proof-checker command wrap-induct for an example of the use of wrap.