blob: 61dd68f6605f558e94bf6fb35ae9deb3587a386b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(in-package "ACL2")
(defconst *import-symbols*
(set-difference-eq
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*)
'(null + * - < = / commutativity-of-* associativity-of-*
commutativity-of-+ associativity-of-+ distributivity)))
(defpkg "FUTER"
*import-symbols*)
(certify-book "futermino" ? t)
|
