IN-PACKAGE

select current package
Major Section:  MISCELLANEOUS

Example:
(in-package "MY-PKG")

General Form: (in-package str)

where str is a string that names an existing ACL2 package, i.e., one of the initial packages such as "KEYWORD" or "ACL2" or a package introduced with defpkg. For a complete list of the known packages created with defpkg, evaluate
(strip-cars (known-package-alist state)).
See defpkg. In-package forms can only be typed at the top-level of the ACL2 loop and as the first form in a file being loaded or compiled.