sub2 - ACL2 Book

Included Books

pkg2

other

(in-package "ACL2")

a-in-acl2-pkgencapsulate

(encapsulate nil
  (local (include-book "pkg2"))
  (defthm a-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))
        "ACL2"))
    :rule-classes nil))