equal
deleted
inserted
replaced
3 # |
3 # |
4 |
4 |
5 ## targets |
5 ## targets |
6 |
6 |
7 default: HOL |
7 default: HOL |
8 generate: HOL-Complex-Generate-HOL |
8 generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight |
9 images: HOL HOL-Algebra HOL-Complex TLA HOL4 |
9 images: HOL HOL-Algebra HOL-Complex TLA HOL4 |
10 |
10 |
11 #Note: keep targets sorted (except for HOL-Library) |
11 #Note: keep targets sorted (except for HOL-Library) |
12 test: \ |
12 test: \ |
13 HOL-Library \ |
13 HOL-Library \ |
266 Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \ |
266 Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \ |
267 Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy \ |
267 Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy \ |
268 Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML |
268 Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML |
269 @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL |
269 @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL |
270 |
270 |
|
271 |
|
272 ## HOL-Complex-Generate-HOLLight |
|
273 |
271 HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz |
274 HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz |
272 |
275 |
273 $(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \ |
276 $(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \ |
274 Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML |
277 Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML |
275 @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight |
278 @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight |
|
279 |
276 |
280 |
277 ## HOL-Import-HOL |
281 ## HOL-Import-HOL |
278 |
282 |
279 HOL4: HOL-Complex $(LOG)/HOL4.gz |
283 HOL4: HOL-Complex $(LOG)/HOL4.gz |
280 |
284 |