diff options
Diffstat (limited to 'books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.acl2')
-rw-r--r-- | books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.acl2 | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.acl2 b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.acl2 new file mode 100644 index 0000000..3a3b5d1 --- /dev/null +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.acl2 @@ -0,0 +1,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 "fuproducto" ? t) + |