ACL2-PC::PROMOTE

(primitive) move antecedents of conclusion's implies term to top-level hypotheses
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
promote
(promote t)
For example, if the conclusion is (implies (and x y) z), then after execution of promote, the conclusion will be z and the terms x and y will be new top-level hypotheses.

General Form:
(promote &optional do-not-flatten-flag)
Replace conclusion of (implies hyps exp) or (if hyps exp t) with simply exp, adding hyps to the list of top-level hypotheses. Moreover, if hyps is viewed as a conjunction then each conjunct will be added as a separate top-level hypothesis. An exception is that if do-not-flatten-flag is supplied and not nil, then only one top-level hypothesis will be added, namely hyps.

Note: You must be at the top of the conclusion in order to use this command. Otherwise, first invoke top.