intern-in-package-of-symbol

Included Books

other

(in-package "ACL2")

include-book

(include-book "../basic/intern-in-package-of-symbol")