books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

(value :q)

(LP)

(defpkg "S"
  (set-difference-equal
   (union-eq '(PACK
               ORDINARYP
               <<
               <<-IRREFLEXIVITY
               <<-TRICHOTOMY
               <<-MUTUAL-EXCLUSION
               <<-TRANSITIVITY
               FAST-<<-TRICHOTOMY
               FAST-<<-MUTUAL-EXCLUSION
               FAST-<<-TRANSITIVITY
               FAST-<<-RULES
               SLOW-<<-RULES
               <<-RULES)
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))
   '(union intersection subsetp add-to-set functionp = apply)))

(certify-book "set-theory-original" ? t)