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:


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

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage