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.