← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.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/2007/rubio/support/simplicial-topology/generate-degenerate.acl2
 
1
(in-package "ACL2")
 
2
 
 
3
(defconst *abstract-proofs-exports* 
 
4
  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
 
5
    first-of-proof last-of-proof steps-up steps-down steps-valley
 
6
    proof-before-valley proof-after-valley inverse-r-step inverse-proof
 
7
    local-peak-p proof-measure proof-before-peak proof-after-peak
 
8
    local-peak peak-element))
 
9
 
 
10
(defconst *cnf-package-exports*
 
11
  (union-eq *acl2-exports*
 
12
            (union-eq
 
13
             *common-lisp-symbols-from-main-lisp-package*
 
14
             *abstract-proofs-exports*)))
 
15
 
 
16
(defpkg "CNV" (cons 'multiset-diff *cnf-package-exports*))
 
17
 
 
18
 
 
19
(certify-book "generate-degenerate" ? t)