/usr/share/acl2-7.2dfsg/books/make-event/acl2x-help-test.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | (in-package "ACL2")
;; Yes, this include-book may be local even though we'll use macros defined in
;; it, in an apparently nonlocal manner.
(local (include-book "acl2x-help"))
;; If the acl2x-expansion-alist-replacement attachment necessary for the
;; functioning of acl2x-replace has been removed, this replaces it.
;; (use-acl2x-replace)
(acl2x-replace
;; this is only run during pass 1 of certification
(skip-proofs (defthm pass1-only (equal t nil) :rule-classes nil))
;; this is run except during pass 1.
(defthm pass2-and-otherwise
(equal x x) :rule-classes nil))
|