Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

1 files changed, 24 insertions, 0 deletions

diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2
new file mode 100644
index 0000000..6ff70ab
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2
@@ -0,0 +1,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)