← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/cowles-gamboa-euclid/Euclid/certify.lsp

  • 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/2006/cowles-gamboa-euclid/Euclid/certify.lsp
 
1
 
 
2
(in-package "ACL2")
 
3
 
 
4
(defpkg "POS"
 
5
  (union-eq *acl2-exports*
 
6
            *common-lisp-symbols-from-main-lisp-package*))
 
7
 
 
8
(certify-book "prime-fac" 
 
9
              1
 
10
              )
 
11
:u :u
 
12
 
 
13
(DEFPKG "ACL2-ASG"
 
14
  (SET-DIFFERENCE-EQUAL
 
15
   (UNION-EQ *ACL2-EXPORTS* 
 
16
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
17
   '(ZERO)))
 
18
 
 
19
(certify-book "ed1" 
 
20
              1   
 
21
              nil ;;compile-flg
 
22
              )
 
23
:u :u
 
24
 
 
25
(certify-book "ed2a" 
 
26
              0   
 
27
              nil ;;compile-flg
 
28
              )
 
29
:u
 
30
 
 
31
(certify-book "ed2b")
 
32
:u
 
33
 
 
34
(DEFPKG "ACL2-ASG"
 
35
  (SET-DIFFERENCE-EQUAL
 
36
   (UNION-EQ *ACL2-EXPORTS* 
 
37
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
38
   '(ZERO)))
 
39
 
 
40
(DEFPKG "ACL2-AGP"
 
41
  (SET-DIFFERENCE-EQUAL
 
42
   (UNION-EQ *ACL2-EXPORTS* 
 
43
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
44
   '(ZERO)))
 
45
 
 
46
(DEFPKG "ACL2-CRG"
 
47
  (SET-DIFFERENCE-EQUAL
 
48
   (UNION-EQ *ACL2-EXPORTS* 
 
49
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
50
   '(ZERO)))
 
51
 
 
52
(certify-book "ed3"
 
53
              3   
 
54
              nil ;;compile-flg
 
55
              )
 
56
:u :u :u :u
 
57
 
 
58
(defpkg "INT-MOD"
 
59
        (union-eq *acl2-exports*
 
60
                  *common-lisp-symbols-from-main-lisp-package*))
 
61
 
 
62
(certify-book "ed4aa" 
 
63
              1
 
64
              nil ;;compile-flg
 
65
              )
 
66
:u :u
 
67
 
 
68
(defpkg "INT-MOD"
 
69
        (union-eq *acl2-exports*
 
70
                  *common-lisp-symbols-from-main-lisp-package*))
 
71
 
 
72
(certify-book "ed4ab" 
 
73
              1)
 
74
:u :u
 
75
 
 
76
(defpkg "INT-REM"
 
77
        (union-eq *acl2-exports*
 
78
                  *common-lisp-symbols-from-main-lisp-package*))
 
79
 
 
80
(certify-book "ed4ba" 
 
81
              1
 
82
              nil ;;compile-flg
 
83
              )
 
84
:u :u
 
85
 
 
86
(defpkg "INT-REM"
 
87
        (union-eq *acl2-exports*
 
88
                  *common-lisp-symbols-from-main-lisp-package*))
 
89
 
 
90
(certify-book "ed4bb" 
 
91
              1)
 
92
:u :u
 
93
 
 
94
(defpkg "INT-C-MOD"
 
95
        (union-eq *acl2-exports*
 
96
                  *common-lisp-symbols-from-main-lisp-package*))
 
97
 
 
98
(certify-book "ed4ca" 
 
99
              1
 
100
              nil ;;compile-flg
 
101
              )
 
102
:u :u
 
103
 
 
104
(defpkg "INT-C-MOD"
 
105
        (union-eq *acl2-exports*
 
106
                  *common-lisp-symbols-from-main-lisp-package*))
 
107
 
 
108
(certify-book "ed4cb" 
 
109
              1)
 
110
:u :u
 
111
 
 
112
(defpkg "INT-RND-REM"
 
113
        (union-eq *acl2-exports*
 
114
                  *common-lisp-symbols-from-main-lisp-package*))
 
115
 
 
116
(certify-book "ed4da" 
 
117
              1
 
118
              nil ;;compile-flg
 
119
              )
 
120
:u :u
 
121
 
 
122
(defpkg "INT-RND-REM"
 
123
        (union-eq *acl2-exports*
 
124
                  *common-lisp-symbols-from-main-lisp-package*))
 
125
 
 
126
(certify-book "ed4db" 
 
127
              1
 
128
              )
 
129
:u :u
 
130
 
 
131
(defpkg "GAUSS-INT"
 
132
        (union-eq *acl2-exports*
 
133
                  *common-lisp-symbols-from-main-lisp-package*))
 
134
 
 
135
(certify-book "ed5aa" 
 
136
              1
 
137
              nil ;;compile-flg
 
138
              )
 
139
:u :u
 
140
 
 
141
(defconst *import-symbols*
 
142
  (set-difference-eq
 
143
   (union-eq *acl2-exports*
 
144
             *common-lisp-symbols-from-main-lisp-package*)
 
145
     '(null + * - < = / commutativity-of-* associativity-of-* 
 
146
            commutativity-of-+ associativity-of-+ distributivity)))
 
147
 
 
148
(defpkg "FLD"
 
149
  *import-symbols*)
 
150
 
 
151
(defpkg "FUTER"
 
152
  *import-symbols*)
 
153
 
 
154
(defpkg "FUMON"
 
155
  (union-eq *import-symbols*
 
156
            '(FLD::fdp FUTER::terminop)))
 
157
 
 
158
(defpkg "FUPOL"
 
159
  (union-eq *import-symbols*
 
160
            '(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
 
161
                            FUMON::termino FUMON::monomiop)))
 
162
 
 
163
(defpkg "FUNPOL"
 
164
  (set-difference-eq *import-symbols*
 
165
                     '(rem)))
 
166
 
 
167
(certify-book "ed6a" 
 
168
              6
 
169
              nil ;;compile-flg
 
170
              )
 
171
:u :u :u :u :u :u :u
 
172