PROOF-COMMENT : MEXPR

PROOF-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:

 <n>PROOF-COMMENT  COMMENT 
"STRING"


The arguments have the following meaning:
COMMENT : Comment to attach to proof

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage