GET-OUTPUT-STREAM-STRING$
See
io
.
Major Section:
ACL2-BUILT-INS
