summaryrefslogtreecommitdiff
path: root/books/workshops/2004/smith-et-al/support/bags/bag-pkg.acl2
blob: e8e930926667d6dd41aefcac71b52195701fb8e4 (plain)
1
2
3
4
5
6
7
8
9
10
11
(include-book "../lists/list-exports")
(include-book "../syntax/syn-pkg")
(defpkg "BAG" (append '(syn::defirrelevant
			syn::defignore 
			syn::defignored 
			mfc-clause 
			mfc-ancestors 
			let 
			term-order) 
		      *acl2-exports* list::*exports*))
(certify-book "bag-pkg" ? t)