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