wrap.
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.