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:

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.