Pkg-witness
Return a specific symbol in the indicated package
For any string pkg that names a package currently known to
ACL2, (pkg-witness pkg) is a symbol in that package whose symbol-name is the value of constant *pkg-witness-name*. Logically,
this is the case even if the package is not currently known to ACL2. However,
if pkg-witness is called on a string that is not the name of a package
known to ACL2, a hard Lisp error will result.
(Pkg-witness pkg) has a guard of (and (stringp pkg) (not (equal pkg
""))). If pkg is not a string, then (pkg-witness pkg) is equal
to (pkg-witness "ACL2")
