blob: 78cee74af20bd0c4724c84c2a6a40c009d1f4025 (
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
25
26
|
(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 "FLD"
*import-symbols*)
(defpkg "FUTER"
*import-symbols*)
(defpkg "FUMON"
(union-eq *import-symbols*
'(FLD::fdp FUTER::terminop)))
(defpkg "FUPOL"
(union-eq *import-symbols*
'(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
FUMON::termino FUMON::monomiop)))
(certify-book "fuopuesto" ? t)
|
