ACL2-PC::RETAIN

(atomic macro) drop all but the indicated top-level hypotheses 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(RETAIN 2 3) -- keep the second and third hypotheses, and drop
                the rest

General Form:
(retain &rest args)
Drop all top-level hypotheses except those with the indicated indices.

There must be at least one argument, and all must be in range (i.e. integers between one and the number of top-level hypotheses, inclusive).