equal
deleted
inserted
replaced
22 ## FOLP |
22 ## FOLP |
23 |
23 |
24 FOLP: Pure $(OUT)/FOLP |
24 FOLP: Pure $(OUT)/FOLP |
25 |
25 |
26 Pure: |
26 Pure: |
27 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
27 @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure |
28 |
28 |
29 $(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML \ |
29 $(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML \ |
30 hypsubst.ML intprover.ML simp.ML simpdata.ML |
30 hypsubst.ML intprover.ML simp.ML simpdata.ML |
31 @$(ISATOOL) usedir -b $(OUT)/Pure FOLP |
31 @$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP |
32 |
32 |
33 |
33 |
34 ## FOLP-ex |
34 ## FOLP-ex |
35 |
35 |
36 FOLP-ex: FOLP $(LOG)/FOLP-ex.gz |
36 FOLP-ex: FOLP $(LOG)/FOLP-ex.gz |
38 $(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy \ |
38 $(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy \ |
39 ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy \ |
39 ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy \ |
40 ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy \ |
40 ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy \ |
41 ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \ |
41 ex/Propositional_Cla.thy ex/Quantifiers_Int.thy \ |
42 ex/Quantifiers_Cla.thy |
42 ex/Quantifiers_Cla.thy |
43 @$(ISATOOL) usedir $(OUT)/FOLP ex |
43 @$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex |
44 |
44 |
45 |
45 |
46 ## clean |
46 ## clean |
47 |
47 |
48 clean: |
48 clean: |