← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.acl2

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.acl2
 
1
(in-package "ACL2")
 
2
 
 
3
(defconst *import-symbols*
 
4
  (set-difference-eq
 
5
   (union-eq *acl2-exports*
 
6
             *common-lisp-symbols-from-main-lisp-package*)
 
7
     '(null + * - < = / commutativity-of-* associativity-of-* 
 
8
            commutativity-of-+ associativity-of-+ distributivity)))
 
9
 
 
10
(defpkg "FLD"
 
11
  *import-symbols*)
 
12
 
 
13
(defpkg "FUTER"
 
14
  *import-symbols*)
 
15
 
 
16
(defpkg "FUMON"
 
17
  (union-eq *import-symbols*
 
18
            '(FLD::fdp FUTER::terminop)))
 
19
 
 
20
(defpkg "FUPOL"
 
21
  (union-eq *import-symbols*
 
22
            '(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
 
23
                            FUMON::termino FUMON::monomiop)))
 
24
 
 
25
(certify-book "fupolinomio" ? t)
 
26