intern-in-package-of-symbol

(in-package "ACL2")

(defsection std/basic/intern-in-package-of-symbol
  :parents (std/basic intern-in-package-of-symbol)
  :short "Lemmas about @(see intern-in-package-of-symbol) available in the
  @(see std/basic) library."
  (local (defthm intern-in-package-of-symbol-lemma
      (implies (and (stringp a)
          (stringp b)
          (symbolp in-pkg)
          (not (equal a b)))
        (not (equal (intern-in-package-of-symbol a in-pkg)
            (intern-in-package-of-symbol b in-pkg))))
      :hints (("Goal" :use ((:instance symbol-name-intern-in-package-of-symbol
            (s a)
            (any-symbol in-pkg)) (:instance symbol-name-intern-in-package-of-symbol
             (s b)
             (any-symbol in-pkg)))))))
  (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)))))