IN-PACKAGE
select current package
Major Section: OTHER
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. An ACL2 book (see books) must contain a single in-package
form, which must be the first form in that book.
