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.