ACL2-PC::PRO

(atomic macro) repeatedly apply promote
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
pro

Apply the promote command until there is no change. This command ``succeeds'' exactly when at least one call of promote ``succeeds''. In that case, only a single new proof-checker state will be created.