DOC!

all the documentation for a name (type :doc! name)
Major Section:  DOCUMENTATION

NOTE: The :doc! command only makes sense at the terminal.

Examples:
ACL2 !>:doc! defthm
ACL2 !>:doc! certificate

This command is like :doc name followed by :more!. It prints all the documentation of name.