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
instrsare executed, as in
do-all. If this ``fails'' then no additional action is taken. Otherwise, the current goal after execution of
instrsis conjoined with all ``new'' goals, in the sense that their names are not among the names of goals at the time
instrswas 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