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.
