equal
deleted
inserted
replaced
14 |
14 |
15 SRC = $(ISABELLE_HOME)/src |
15 SRC = $(ISABELLE_HOME)/src |
16 OUT = $(ISABELLE_OUTPUT) |
16 OUT = $(ISABELLE_OUTPUT) |
17 LOG = $(OUT)/log |
17 LOG = $(OUT)/log |
18 USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL |
18 USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL |
|
19 REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real |
19 |
20 |
20 ## HOL |
21 ## HOL |
21 |
22 |
22 HOL: |
23 HOL: |
23 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
24 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
|
25 |
|
26 HOL-Real: |
|
27 @cd $(SRC)/HOL; $(ISATOOL) make HOL-Real |
24 |
28 |
25 styles: |
29 styles: |
26 @rm -f isabelle.sty |
30 @rm -f isabelle.sty |
27 @rm -f isabellesym.sty |
31 @rm -f isabellesym.sty |
28 @rm -f pdfsetup.sty |
32 @rm -f pdfsetup.sty |
143 $(USEDIR) Inductive |
147 $(USEDIR) Inductive |
144 @rm -f tutorial.dvi |
148 @rm -f tutorial.dvi |
145 |
149 |
146 ## HOL-Types |
150 ## HOL-Types |
147 |
151 |
148 HOL-Types: HOL $(LOG)/HOL-Types.gz |
152 HOL-Types: HOL-Real $(LOG)/HOL-Types.gz |
149 |
153 |
150 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \ |
154 $(LOG)/HOL-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \ |
151 Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \ |
155 Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \ |
152 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ |
156 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ |
153 Types/Overloading.thy Types/Axioms.thy |
157 Types/Overloading.thy Types/Axioms.thy |
154 $(USEDIR) Types |
158 $(REALUSEDIR) Types |
155 @rm -f tutorial.dvi |
159 @rm -f tutorial.dvi |
156 |
160 |
157 ## HOL-Misc |
161 ## HOL-Misc |
158 |
162 |
159 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
163 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |