19 LOG = $(OUT)/log |
19 LOG = $(OUT)/log |
20 |
20 |
21 |
21 |
22 ## FOL |
22 ## FOL |
23 |
23 |
24 FOL: Pure $(OUT)/FOL$(ML_SUFFIX) |
24 FOL: Pure $(OUT)/FOL |
25 |
25 |
26 Pure: |
26 Pure: |
27 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
27 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
28 |
28 |
29 $(OUT)/Pure$(ML_SUFFIX): Pure |
29 $(OUT)/Pure: Pure |
30 |
30 |
31 $(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML \ |
31 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ |
32 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
32 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
33 $(SRC)/Tools/IsaPlanner/zipper.ML \ |
33 $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \ |
34 $(SRC)/Tools/IsaPlanner/isand.ML \ |
34 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
35 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
35 $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Provers/eqsubst.ML \ |
36 $(SRC)/Tools/IsaPlanner/rw_inst.ML \ |
36 $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ |
37 $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ |
37 $(SRC)/Tools/atomize_elim.ML $(SRC)/Provers/project_rule.ML \ |
38 $(SRC)/Tools/induct.ML $(SRC)/Tools/atomize_elim.ML \ |
38 $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy \ |
39 $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
39 IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex \ |
40 $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML \ |
40 fologic.ML hypsubstdata.ML intprover.ML simpdata.ML |
41 document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML |
|
42 @$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL |
41 @$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL |
43 |
42 |
44 |
43 |
45 ## FOL-ex |
44 ## FOL-ex |
46 |
45 |
47 FOL-ex: FOL $(LOG)/FOL-ex.gz |
46 FOL-ex: FOL $(LOG)/FOL-ex.gz |
48 |
47 |
49 $(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \ |
48 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ |
50 ex/If.thy ex/IffOracle.thy ex/LocaleTest.thy \ |
49 ex/IffOracle.thy ex/LocaleTest.thy ex/Nat.thy ex/Natural_Numbers.thy \ |
51 ex/Nat.thy ex/Natural_Numbers.thy ex/Miniscope.thy \ |
50 ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \ |
52 ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \ |
51 ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \ |
53 ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy \ |
52 ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \ |
54 ex/Propositional_Int.thy ex/Propositional_Cla.thy \ |
|
55 ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy |
53 ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy |
56 @$(ISATOOL) usedir $(OUT)/FOL ex |
54 @$(ISATOOL) usedir $(OUT)/FOL ex |
57 |
55 |
58 |
56 |
59 ## clean |
57 ## clean |
60 |
58 |
61 clean: |
59 clean: |
62 @rm -f $(OUT)/FOL$(ML_SUFFIX) $(LOG)/FOL.gz $(LOG)/FOL-ex.gz |
60 @rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz |