equal
deleted
inserted
replaced
22 ## CTT |
22 ## CTT |
23 |
23 |
24 CTT: Pure $(OUT)/CTT |
24 CTT: Pure $(OUT)/CTT |
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)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \ |
29 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \ |
30 Bool.thy CTT.thy Main.thy ROOT.ML rew.ML |
30 Bool.thy CTT.thy Main.thy ROOT.ML rew.ML |
31 @$(ISATOOL) usedir -b $(OUT)/Pure CTT |
31 @$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT |
32 |
32 |
33 |
33 |
34 ## CTT-ex |
34 ## CTT-ex |
35 |
35 |
36 CTT-ex: CTT $(LOG)/CTT-ex.gz |
36 CTT-ex: CTT $(LOG)/CTT-ex.gz |
37 |
37 |
38 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \ |
38 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \ |
39 ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy |
39 ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy |
40 @$(ISATOOL) usedir $(OUT)/CTT ex |
40 @$(ISABELLE_TOOL) usedir $(OUT)/CTT ex |
41 |
41 |
42 |
42 |
43 ## clean |
43 ## clean |
44 |
44 |
45 clean: |
45 clean: |