; acl2 < script > script.log & (DEFPKG "TJVM" (set-difference-equal (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<) (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)) '(PC PROGRAM PUSH POP REVERSE STEP ++))) (certify-book "tjvm" 1) (u) (u) (include-book "/v/hank/v104/text/defpun/tjvm") (certify-book "examples" 1) (u) (u) (certify-book "defpun") (u) (certify-book "mod-1-property") (u) (include-book "/v/hank/v104/text/defpun/examples") (certify-book "tjvm-examples" 1) (u) (u) (certify-book "report")