same as induct, but create a single goal
Major Section: PROOF-CHECKER-COMMANDS
Examples: wrap-induct (wrap-induct t) (wrap-induct (append (reverse x) y)) General Form: (wrap-induct &optional term)The
wrap-induct command is identical to the proof-checker
induct command, except that only a single goal is created: the
conjunction of the base and induction steps.Note: The output will generally indicate that more than goal has been created, e.g.:
Creating two new goals: (MAIN . 1) and (MAIN . 2).However,
wrap-induct always creates a unique goal (when it succeeds). A
subsequent message clarifies this, for example:
NOTE: Created ONLY one new goal, which is the current goal: (MAIN . 1)
