(IN-PACKAGE "ACL2") "ACL2 Version 2.7" :BEGIN-PORTCULLIS-CMDS :END-PORTCULLIS-CMDS NIL (("/v/net2/v2/users/prof/moore/publications/trecia/support/defpun.lisp" "defpun" "defpun" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143438860)) 129300060