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

(certify-book "basic-pkg-check" 1)