Definition:
(defconst *atj-gen-pkg-name-alist* '(("KEYWORD" . "Acl2PackageName.KEYWORD") ("COMMON-LISP" . "Acl2PackageName.LISP") ("ACL2" . "Acl2PackageName.ACL2") ("ACL2-OUTPUT-CHANNEL" . "Acl2PackageName.ACL2_OUTPUT") ("ACL2-INPUT-CHANNEL" . "Acl2PackageName.ACL2_INPUT") ("ACL2-PC" . "Acl2PackageName.ACL2_PC") ("ACL2-USER" . "Acl2PackageName.ACL2_USER")))