(ld "rewrite-code-pkg.lsp")


(ACL2::CERTIFY-BOOK "rewrite-code" ACL2::?)