Proofs-co
The proofs character output channel
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*.
