ACL2-pc::promote
(primitive) move antecedents of conclusion's implies term to
top-level hypotheses
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.
Remark: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke top.
