Major Section: MISCELLANEOUS
Example: (in-package "MY-PKG")where
General Form: (in-package str)
stris a string that names an existing ACL2 package, i.e., one of the initial packages such as
"ACL2"or a package introduced with
defpkg. For a complete list of the known packages created with
(strip-cars (known-package-alist state)).See defpkg.
In-packageforms can only be typed at the top-level of the ACL2 loop and as the first form in a file being loaded or compiled.