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 theoremTo use
such a General Form: any theorem :generalizerule, the system
waits until it has decided to generalize some term, term, by
replacing it with some new variable v. If any :generalizeformula
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 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.''