Major Section: DEFPKG
Jared Davis has contributed documentation on managing ACL2 packages. See http://www.cs.utexas.edu/users/moore/acl2/contrib/managing-acl2-packages.html.