ACL2-pc::wrap
(atomic macro)
execute the indicated instructions and combine all the new goals
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 interactive proof-builder command,
wrap-induct, for an example of the use of wrap.
