equal
deleted
inserted
replaced
27 |
27 |
28 $(OUT)/Pure: Pure |
28 $(OUT)/Pure: Pure |
29 |
29 |
30 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ |
30 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ |
31 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
31 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
32 $(SRC)/Tools/case_product.ML \ |
32 $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \ |
33 $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \ |
33 $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
34 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
|
35 $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ |
34 $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ |
36 $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ |
35 $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ |
37 $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ |
36 $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ |
38 $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
37 $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ |
39 $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \ |
38 $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \ |
40 document/root.tex fologic.ML hypsubstdata.ML intprover.ML \ |
39 document/root.tex fologic.ML hypsubstdata.ML intprover.ML \ |
41 simpdata.ML |
40 simpdata.ML |
42 @$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL |
41 @$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL |
43 |
42 |
44 |
43 |