books/workshops/2000/ruiz/multiset/defmul.acl2


1
2
3
4
5
6
7
8
9
10
11

(value :q)
(lp)

(defpkg "MUL" (union-eq *acl2-exports* 
			(union-eq 
			 *common-lisp-symbols-from-main-lisp-package* 
			 '(remove-one multiset-diff 
			   make-ord e0-ordinalp e0-ord-<
			   ctoa atoc))))

(certify-book "defmul" ? t)