## GENERALIZE

make a rule to restrict generalizations
Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which a `:generalize`

rule might be built is:

Example:
any theorem
General Form:
any theorem

To use such a `:generalize`

rule, the system waits until it has
decided to generalize some term, `term`

, by replacing it with some new
variable `v`

. If any `:generalize`

formula can be instantiated so that
some non-variable subterm becomes `term`

, then that instance of the
formula is added as a hypothesis.At the moment, the best description of how ACL2 `:generalize`

rules
are used may be found in the discussion of ``Generalize Rules,'' page
248 of A Computational Logic Handbook, or ``Generalization,'' page
132 of ``Computer-Aided Reasoning: An Approach.'' Also
see introduction-to-the-theorem-prover for detailed tutorial on using ACL2
to prove theorems, which includes some discussion of generalization.