blob: 6ff70abc6886db5fd84ae59b10a130fbd04bcc83 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
;;; --------
;;; Packages
;;; --------
(defconst *acl2-and-lisp-exports*
(set-difference-eq ; modified 5/26/2015 by Matt K.
(union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
'(termp)))
(defpkg "TER"
(set-difference-eq *acl2-and-lisp-exports* '(<)))
(defpkg "MON"
(union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
'(TER::termp TER::term->o-p)))
(defpkg "UPOL"
(union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
(defpkg "NPOL"
(union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
'(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
(certify-book "term" ? t)
|
