Major Section: ACL2-BUILT-INS
Intern$ is a macro that behaves the same as the macro intern,
except for weakening the restriction to a fixed set of package names so that
any package name other than "" is legal. See intern. Note that if you
evaluate a call (intern$ x y) for which there is no package with name
y that is known to ACL2, you will get an error.
(Intern$ x y) expands to:
(intern-in-package-of-symbol x (pkg-witness y))See intern-in-package-of-symbol and see pkg-witness.
