INTERN$

create a new symbol in a given package
Major Section:  PROGRAMMING

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.