ACL2-PC::INDUCT

(atomic macro) generate subgoals using induction
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
induct, (induct t)
   -- induct according to a heuristically-chosen scheme, creating
      a new subgoal for each base and induction step
(induct (append (reverse x) y))
   -- as above, but choose an induction scheme based on the term
      (append (reverse x) y) rather than on the current goal

General Form: (induct &optional term)

Induct as in the corresponding :induct hint given to the theorem prover, creating new subgoals for the base and induction steps. If term is t or is not supplied, then use the current goal to determine the induction scheme; otherwise, use that term.

Note: As usual, abbreviations are allowed in the term.

Note: Induct actually calls the prove command with all processes turned off. Thus, you must be at top of the goal for an induct instruction.