top.
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.