equal
deleted
inserted
replaced
3 # |
3 # |
4 # IsaMakefile for FOLP |
4 # IsaMakefile for FOLP |
5 # |
5 # |
6 |
6 |
7 OUT = $(ISABELLE_OUTPUT) |
7 OUT = $(ISABELLE_OUTPUT) |
|
8 LOG = $(OUT)/log |
8 |
9 |
9 FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \ |
10 FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \ |
10 hypsubst.ML classical.ML simp.ML |
11 hypsubst.ML classical.ML simp.ML |
11 |
12 |
12 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \ |
13 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \ |
17 @$(ISATOOL) usedir -b $(OUT)/Pure FOLP |
18 @$(ISATOOL) usedir -b $(OUT)/Pure FOLP |
18 |
19 |
19 $(OUT)/Pure: |
20 $(OUT)/Pure: |
20 @cd ../Pure; $(ISATOOL) make |
21 @cd ../Pure; $(ISATOOL) make |
21 |
22 |
22 test: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) |
23 $(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) |
23 @$(ISATOOL) usedir $(OUT)/FOLP ex |
24 @$(ISATOOL) usedir $(OUT)/FOLP ex |
24 |
25 |
|
26 test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz |
|
27 |
|
28 clean: |
|
29 @rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz |
|
30 |
|
31 |
25 .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP |
32 .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP |