PROOF-COMMENT : MEXPRPROOF-COMMENT is a top-level command.
Attaches a comment to the current proof.
The default value is the current comment. Uses the same
comment syntax as LINE-COMMENT; see the help message of that command
for more information. You can see the comments on all the
current proofs by using PROOFLIST.
The command format for PROOF-COMMENT is:
The arguments have the following meaning:
COMMENT : Comment to attach to proof
TPS documentation homepage