6
'(value er-let* er-decode-logical-name getprop current-acl2-world
7
stobjs-in cltl-command global-value soft)
11
compute-copy-defun+rewrite
12
assert-include-defun-matches-certify-defun
15
(union-eq *acl2-exports*
16
*common-lisp-symbols-from-main-lisp-package*)))
18
(certify-book "rewrite-code" ? t)