ACL2-pc::pro
(atomic macro)
repeatedly apply promote
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-builder state will be created.
Note: The split command is probably more helpful in many cases than
pro.
