available documentation topics (by section)

NOTE: The :docs command only makes sense at the terminal.

ACL2 !>:docs *           ; lists documentation sections
ACL2 !>:docs **          ; lists all documented topics within all sections
ACL2 !>:docs events      ; lists all topics in section EVENTS
ACL2 !>:docs "compil"    ; lists topics ``apropos''

The data base of formatted documentation strings is structured into sections. Within a section are topics. Each topic has a one-liner, some notes, and some detailed discussions. The :docs command provides a view of the entire data base.

:docs takes one argument, as described below:

arg               effect

* list all section headings in the data base ** list all section headings and all topics within each section name list all topics in the section named name (where name is some symbol other than * and **). This is always the same as :doc name. pattern list all topics whose :doc or :more-doc text mentions the string pattern. For purposes of this string matching we ignore distinctions of case and the amount and kind (but not presence) of white space. We also treat hyphen as whitespace.