sub1 - ACL2 Book

Included Books

pkg1

other

(in-package "ACL2")

a-not-in-acl2-pkgencapsulate

(encapsulate nil
  (local (include-book "pkg1"))
  (defthm a-not-in-acl2-pkg
    (implies (and (symbolp x) (equal (symbol-package-name x) "MY-PKG"))
      (equal (symbol-package-name (intern-in-package-of-symbol "A" x))
        "MY-PKG"))
    :rule-classes nil))