← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/Makefile

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/arithmetic/Makefile
 
1
include ../../../Makefile-generic
 
2
ACL2 = ../../../../saved_acl2
 
3
 
 
4
 
 
5
# don't alphabetize this!
 
6
BOOKS = ground-zero induct predicate rationalp negative-syntaxp integerp inverted-factor fp2 fp arith2 arith denominator numerator unary-divide product-proofs product nniq basic cg complex-rationalp even-odd  expt-proofs expt expo expo-proofs fl-proofs fl fl-expt floor floor-proofs hacks mod-proofs mod mod-expt power2p product unary-divide x-2xx even-odd2-proofs even-odd2 fl-hacks top extra-rules common-factor-defuns common-factor
 
7
 
 
8
# remove float?
 
9
# remove util?
 
10
# remove hacks?
 
11
# remove induct?
 
12
#  land lextra lior log logand logand-proofs logeqv logior logior1 lognot logorc1 logs logxor lxor lnot ash 
 
13
 
 
14
 
 
15
 
 
16
ground-zero.cert: ground-zero.lisp
 
17
 
 
18
induct.cert: induct.lisp
 
19
induct.cert: fl.cert
 
20
 
 
21
predicate.cert: predicate.lisp
 
22
 
 
23
rationalp.cert: rationalp.lisp
 
24
rationalp.cert: predicate.cert
 
25
 
 
26
negative-syntaxp.cert: negative-syntaxp.lisp
 
27
 
 
28
integerp.cert: integerp.lisp
 
29
integerp.cert: negative-syntaxp.cert
 
30
integerp.cert: predicate.cert
 
31
integerp.cert: fp2.cert
 
32
 
 
33
inverted-factor.cert: inverted-factor.lisp
 
34
 
 
35
fp2.cert: fp2.lisp
 
36
fp2.cert: ../../../ihs/ihs-definitions.cert
 
37
fp2.cert: ../../../ihs/ihs-lemmas.cert
 
38
fp2.cert: ../../../ihs/ihs-lemmas.cert
 
39
fp2.cert: ../../../arithmetic-2/meta/non-linear.cert
 
40
fp2.cert: inverted-factor.cert
 
41
fp2.cert: ../../../ordinals/e0-ordinal.cert
 
42
 
 
43
fp.cert: fp.lisp
 
44
fp.cert: fp2.cert
 
45
 
 
46
arith2.cert: arith2.lisp
 
47
arith2.cert: fp2.cert
 
48
arith2.cert: predicate.cert
 
49
arith2.cert: product.cert
 
50
arith2.cert: ../../../meta/meta-times-equal.cert
 
51
arith2.cert: ../../../meta/meta-plus-equal.cert
 
52
arith2.cert: ../../../meta/meta-plus-lessp.cert
 
53
arith2.cert: ../../../meta/meta-times-equal.cert
 
54
arith2.cert: ../../../meta/meta-plus-equal.cert
 
55
arith2.cert: ../../../meta/meta-plus-lessp.cert
 
56
arith2.cert: inverted-factor.cert
 
57
 
 
58
arith.cert: arith.lisp
 
59
arith.cert: arith2.cert
 
60
arith.cert: ../../../meta/meta-plus-equal.cert
 
61
arith.cert: ../../../meta/meta-plus-lessp.cert
 
62
arith.cert: ../../../meta/meta-times-equal.cert
 
63
 
 
64
denominator.cert: denominator.lisp
 
65
denominator.cert: ground-zero.cert
 
66
denominator.cert: fp2.cert
 
67
denominator.cert: ../../../arithmetic/mod-gcd.cert
 
68
 
 
69
numerator.cert: numerator.lisp
 
70
numerator.cert: ground-zero.cert
 
71
numerator.cert: fp2.cert
 
72
numerator.cert: denominator.cert
 
73
numerator.cert: predicate.cert
 
74
 
 
75
unary-divide.cert: unary-divide.lisp
 
76
unary-divide.cert: predicate.cert
 
77
unary-divide.cert: fp2.cert
 
78
unary-divide.cert: inverted-factor.cert
 
79
 
 
80
product-proofs.cert: product-proofs.lisp
 
81
product-proofs.cert: predicate.cert
 
82
product-proofs.cert: fp2.cert
 
83
 
 
84
product.cert: product.lisp
 
85
product.cert: product-proofs.cert
 
86
 
 
87
nniq.cert: nniq.lisp
 
88
nniq.cert: ground-zero.cert
 
89
nniq.cert: fp2.cert
 
90
nniq.cert: denominator.cert
 
91
nniq.cert: numerator.cert
 
92
nniq.cert: predicate.cert
 
93
nniq.cert: unary-divide.cert
 
94
nniq.cert: product.cert
 
95
nniq.cert: integerp.cert
 
96
nniq.cert: arith.cert
 
97
nniq.cert: ../../../arithmetic/rationals.cert
 
98
nniq.cert: ../../../arithmetic/idiv.cert
 
99
nniq.cert: ../../../arithmetic/idiv.cert
 
100
nniq.cert: ../../../arithmetic/top-with-meta.cert
 
101
 
 
102
basic.cert: basic.lisp
 
103
basic.cert: fp2.cert
 
104
basic.cert: even-odd.cert
 
105
basic.cert: fl.cert
 
106
basic.cert: fl.cert
 
107
basic.cert: expt.cert
 
108
 
 
109
cg.cert: cg.lisp
 
110
cg.cert: fl.cert
 
111
cg.cert: fp2.cert
 
112
cg.cert: integerp.cert
 
113
cg.cert: integerp.cert
 
114
cg.cert: arith2.cert
 
115
cg.cert: common-factor.cert
 
116
 
 
117
complex-rationalp.cert: complex-rationalp.lisp
 
118
complex-rationalp.cert: predicate.cert
 
119
 
 
120
even-odd.cert: even-odd.lisp
 
121
even-odd.cert: integerp.cert
 
122
even-odd.cert: predicate.cert
 
123
even-odd.cert: fp2.cert
 
124
 
 
125
expt-proofs.cert: expt-proofs.lisp
 
126
expt-proofs.cert: ground-zero.cert
 
127
expt-proofs.cert: negative-syntaxp.cert
 
128
expt-proofs.cert: predicate.cert
 
129
expt-proofs.cert: fp2.cert
 
130
expt-proofs.cert: numerator.cert
 
131
expt-proofs.cert: denominator.cert
 
132
expt-proofs.cert: integerp.cert
 
133
expt-proofs.cert: fl.cert
 
134
expt-proofs.cert: arith2.cert
 
135
expt-proofs.cert: ../../../arithmetic/top.cert
 
136
expt-proofs.cert: even-odd.cert
 
137
 
 
138
expt.cert: expt.lisp
 
139
expt.cert: ground-zero.cert
 
140
expt.cert: negative-syntaxp.cert
 
141
expt.cert: expt-proofs.cert
 
142
 
 
143
expo.cert: expo.lisp
 
144
expo.cert: ground-zero.cert
 
145
expo.cert: negative-syntaxp.cert
 
146
expo.cert: power2p.cert
 
147
expo.cert: expo-proofs.cert
 
148
expo.cert: common-factor-defuns.cert
 
149
 
 
150
expo-proofs.cert: expo-proofs.lisp
 
151
expo-proofs.cert: negative-syntaxp.cert
 
152
expo-proofs.cert: power2p.cert
 
153
expo-proofs.cert: unary-divide.cert
 
154
expo-proofs.cert: arith2.cert
 
155
expo-proofs.cert: integerp.cert
 
156
expo-proofs.cert: fl.cert
 
157
expo-proofs.cert: expt.cert
 
158
expo-proofs.cert: ../../../ordinals/e0-ordinal.cert
 
159
expo-proofs.cert: common-factor-defuns.cert
 
160
expo-proofs.cert: common-factor.cert
 
161
 
 
162
fl-proofs.cert: fl-proofs.lisp
 
163
fl-proofs.cert: numerator.cert
 
164
fl-proofs.cert: denominator.cert
 
165
fl-proofs.cert: nniq.cert
 
166
fl-proofs.cert: arith2.cert
 
167
fl-proofs.cert: ground-zero.cert
 
168
fl-proofs.cert: floor.cert
 
169
fl-proofs.cert: integerp.cert
 
170
fl-proofs.cert: rationalp.cert
 
171
fl-proofs.cert: unary-divide.cert
 
172
fl-proofs.cert: common-factor.cert
 
173
fl-proofs.cert: negative-syntaxp.cert
 
174
 
 
175
fl.cert: fl.lisp
 
176
fl.cert: negative-syntaxp.cert
 
177
fl.cert: fl-proofs.cert
 
178
 
 
179
fl-expt.cert: fl-expt.lisp
 
180
fl-expt.cert: numerator.cert
 
181
fl-expt.cert: denominator.cert
 
182
fl-expt.cert: nniq.cert
 
183
fl-expt.cert: arith2.cert
 
184
fl-expt.cert: ground-zero.cert
 
185
fl-expt.cert: floor.cert
 
186
fl-expt.cert: integerp.cert
 
187
fl-expt.cert: rationalp.cert
 
188
fl-expt.cert: unary-divide.cert
 
189
fl-expt.cert: expt.cert
 
190
fl-expt.cert: expo.cert
 
191
fl-expt.cert: power2p.cert
 
192
fl-expt.cert: fl.cert
 
193
 
 
194
floor.cert: floor.lisp
 
195
floor.cert: floor-proofs.cert
 
196
 
 
197
floor-proofs.cert: floor-proofs.lisp
 
198
floor-proofs.cert: ground-zero.cert
 
199
floor-proofs.cert: fp2.cert
 
200
floor-proofs.cert: denominator.cert
 
201
floor-proofs.cert: numerator.cert
 
202
floor-proofs.cert: predicate.cert
 
203
floor-proofs.cert: nniq.cert
 
204
floor-proofs.cert: product.cert
 
205
floor-proofs.cert: unary-divide.cert
 
206
floor-proofs.cert: rationalp.cert
 
207
floor-proofs.cert: inverted-factor.cert
 
208
floor-proofs.cert: ../../../meta/meta-plus-lessp.cert
 
209
 
 
210
hacks.cert: hacks.lisp
 
211
hacks.cert: fp2.cert
 
212
 
 
213
mod-proofs.cert: mod-proofs.lisp
 
214
mod-proofs.cert: ground-zero.cert
 
215
mod-proofs.cert: negative-syntaxp.cert
 
216
mod-proofs.cert: floor.cert
 
217
mod-proofs.cert: arith2.cert
 
218
mod-proofs.cert: power2p.cert
 
219
mod-proofs.cert: fp2.cert
 
220
mod-proofs.cert: arith.cert
 
221
mod-proofs.cert: integerp.cert
 
222
mod-proofs.cert: product.cert
 
223
mod-proofs.cert: complex-rationalp.cert
 
224
mod-proofs.cert: ../../../meta/meta-plus-equal.cert
 
225
mod-proofs.cert: ../../../meta/meta-plus-lessp.cert
 
226
mod-proofs.cert: predicate.cert
 
227
mod-proofs.cert: rationalp.cert
 
228
mod-proofs.cert: fl.cert
 
229
 
 
230
mod.cert: mod.lisp
 
231
mod.cert: ground-zero.cert
 
232
mod.cert: negative-syntaxp.cert
 
233
mod.cert: mod-proofs.cert
 
234
mod.cert: fl.cert
 
235
 
 
236
mod-expt.cert: mod-expt.lisp
 
237
mod-expt.cert: power2p.cert
 
238
mod-expt.cert: numerator.cert
 
239
mod-expt.cert: denominator.cert
 
240
mod-expt.cert: nniq.cert
 
241
mod-expt.cert: arith2.cert
 
242
mod-expt.cert: ground-zero.cert
 
243
mod-expt.cert: floor.cert
 
244
mod-expt.cert: integerp.cert
 
245
mod-expt.cert: rationalp.cert
 
246
mod-expt.cert: unary-divide.cert
 
247
mod-expt.cert: expt.cert
 
248
mod-expt.cert: expo.cert
 
249
mod-expt.cert: fl-expt.cert
 
250
mod-expt.cert: mod.cert
 
251
mod-expt.cert: fl.cert
 
252
 
 
253
power2p.cert: power2p.lisp
 
254
power2p.cert: fl.cert
 
255
power2p.cert: fp2.cert
 
256
power2p.cert: predicate.cert
 
257
power2p.cert: unary-divide.cert
 
258
power2p.cert: ../../../ordinals/e0-ordinal.cert
 
259
 
 
260
product.cert: product.lisp
 
261
product.cert: product-proofs.cert
 
262
 
 
263
unary-divide.cert: unary-divide.lisp
 
264
unary-divide.cert: predicate.cert
 
265
unary-divide.cert: fp2.cert
 
266
unary-divide.cert: inverted-factor.cert
 
267
 
 
268
x-2xx.cert: x-2xx.lisp
 
269
x-2xx.cert: ../../../arithmetic/top-with-meta.cert
 
270
x-2xx.cert: ../../../arithmetic/mod-gcd.cert
 
271
 
 
272
even-odd2-proofs.cert: even-odd2-proofs.lisp
 
273
even-odd2-proofs.cert: integerp.cert
 
274
even-odd2-proofs.cert: arith.cert
 
275
even-odd2-proofs.cert: arith2.cert
 
276
even-odd2-proofs.cert: fp2.cert
 
277
 
 
278
even-odd2.cert: even-odd2.lisp
 
279
even-odd2.cert: ground-zero.cert
 
280
even-odd2.cert: even-odd2-proofs.cert
 
281
 
 
282
fl-hacks.cert: fl-hacks.lisp
 
283
fl-hacks.cert: ground-zero.cert
 
284
fl-hacks.cert: inverted-factor.cert
 
285
fl-hacks.cert: nniq.cert
 
286
fl-hacks.cert: numerator.cert
 
287
fl-hacks.cert: denominator.cert
 
288
fl-hacks.cert: fp2.cert
 
289
fl-hacks.cert: predicate.cert
 
290
fl-hacks.cert: product.cert
 
291
fl-hacks.cert: unary-divide.cert
 
292
fl-hacks.cert: rationalp.cert
 
293
fl-hacks.cert: integerp.cert
 
294
fl-hacks.cert: fl.cert
 
295
fl-hacks.cert: mod.cert
 
296
fl-hacks.cert: even-odd.cert
 
297
fl-hacks.cert: ../../../meta/meta-plus-equal.cert
 
298
fl-hacks.cert: arith.cert
 
299
 
 
300
top.cert: top.lisp
 
301
top.cert: ground-zero.cert
 
302
top.cert: induct.cert
 
303
top.cert: denominator.cert
 
304
top.cert: numerator.cert
 
305
top.cert: nniq.cert
 
306
top.cert: complex-rationalp.cert
 
307
top.cert: rationalp.cert
 
308
top.cert: integerp.cert
 
309
top.cert: arith.cert
 
310
top.cert: arith2.cert
 
311
top.cert: fp2.cert
 
312
top.cert: basic.cert
 
313
top.cert: unary-divide.cert
 
314
top.cert: product.cert
 
315
top.cert: inverted-factor.cert
 
316
top.cert: negative-syntaxp.cert
 
317
top.cert: predicate.cert
 
318
top.cert: x-2xx.cert
 
319
top.cert: power2p.cert
 
320
top.cert: expt.cert
 
321
top.cert: expo.cert
 
322
top.cert: fl-hacks.cert
 
323
top.cert: even-odd2.cert
 
324
top.cert: even-odd.cert
 
325
top.cert: floor.cert
 
326
top.cert: fl.cert
 
327
top.cert: cg.cert
 
328
top.cert: mod.cert
 
329
top.cert: fl-expt.cert
 
330
top.cert: mod-expt.cert
 
331
top.cert: common-factor.cert
 
332
 
 
333
extra-rules.cert: extra-rules.lisp
 
334
extra-rules.cert: basic.cert
 
335
 
 
336
common-factor-defuns.cert: common-factor-defuns.lisp
 
337
common-factor-defuns.cert: inverted-factor.cert
 
338
 
 
339
common-factor.cert: common-factor.lisp
 
340
common-factor.cert: ../../../meta/meta-times-equal.cert
 
341
common-factor.cert: ../../../meta/meta-plus-equal.cert
 
342
common-factor.cert: ../../../meta/meta-plus-lessp.cert
 
343
common-factor.cert: common-factor-defuns.cert
 
344
common-factor.cert: predicate.cert
 
345
common-factor.cert: fp2.cert
 
346
common-factor.cert: product.cert