MISCELLANEOUS

a miscellany of documented functions and concepts (often cited in more accessible documentation)
Major Section:  ACL2 Documentation

Perhaps as the system matures this section will become more structured.