(defpkg "FOO"
  (union-eq '(value)
	     (union-eq *acl2-exports*
		       *common-lisp-symbols-from-main-lisp-package*)))

(certify-book "basic-pkg" 1)