ACL2-PC::COMMENT

(primitive) insert a comment 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(comment now begin difficult final goal)


General Form:
(comment &rest x)
This instruction makes no change in the state except to insert the comment instruction.

Some comments can be used to improve the display of commands; see documentation for comm.