LEFT-hand version recommended.

Execute ML command,
or refine or insert a proof-term doc for proof refinement,

or in RED only:

post a THM goal or rule generating new subproofs,

or, if located on a single edit cmd definition, do a complete standard definition including any keyboard bindings.

The command `{(c-n)(m-n)}(c-z)' will advise the user what WOULD happen if `(c-z)' were executed. Often followup with `(c-a)(c-?)' will be needed for more documentation.
doc for ml execution cmds IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html