		Search-engine friendly clone of the ACL2 documentation.

Std/basic/intern-in-package-of-symbol

Lemmas about intern-in-package-of-symbol available in the std/basic library.

Definitions and Theorems

Theorem: equal-of-intern-in-package-of-symbols

(defthm equal-of-intern-in-package-of-symbols
  (implies (and (stringp a)
                (stringp b)
                (symbolp in-pkg))
           (equal (equal (intern-in-package-of-symbol a in-pkg)
                         (intern-in-package-of-symbol b in-pkg))
                  (equal a b))))