25 HOLCF: HOL $(OUT)/HOLCF |
25 HOLCF: HOL $(OUT)/HOLCF |
26 |
26 |
27 HOL: |
27 HOL: |
28 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
28 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
29 |
29 |
30 $(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \ |
30 $(OUT)/HOLCF: $(OUT)/HOL Cfun.ML Cfun.thy \ |
31 Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \ |
31 Cont.ML Cont.thy Cprod.ML Cprod.thy \ |
32 Cprod2.thy Cprod3.ML Cprod3.thy Discrete.thy Fix.ML Fix.thy Fun1.ML \ |
32 Discrete.thy Fix.ML Fix.thy FunCpo.ML \ |
33 Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \ |
33 FunCpo.thy HOLCF.ML HOLCF.thy Lift.ML \ |
34 Lift.thy One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \ |
34 Lift.thy One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy \ |
35 Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \ |
35 ROOT.ML Sprod.ML Sprod.thy \ |
36 Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \ |
36 Ssum.ML Ssum.thy \ |
37 Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \ |
37 Tr.ML Tr.thy Up.ML \ |
38 Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \ |
38 Up.thy adm.ML cont_consts.ML \ |
39 domain/axioms.ML domain/extender.ML domain/interface.ML \ |
39 domain/axioms.ML domain/extender.ML domain/interface.ML \ |
40 domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \ |
40 domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \ |
41 ex/Stream.thy |
41 ex/Stream.thy |
42 @$(ISATOOL) usedir -b -r $(OUT)/HOL HOLCF |
42 @$(ISATOOL) usedir -b -r $(OUT)/HOL HOLCF |
43 |
43 |