Major Section: ACL2-BUILT-INS
Proofs-co is an ld special (see ld). The accessor is
(proofs-co state) and the updater is (set-proofs-co val state).
Proofs-co must be an open character output channel. It is to this
channel that defun, defthm, and the other event commands print their
commentary.
``Proofs-co'' stands for ``proofs character output.'' The initial
value of proofs-co is the same as the value of *standard-co*
(see *standard-co*).
