equal
deleted
inserted
replaced
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 Adm.thy Cfun.thy Cont.thy Cprod.thy \ |
30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Bifinite.thy Cfun.thy \ |
31 Discrete.thy Domain.thy Ffun.thy Fix.thy Fixrec.thy HOLCF.thy Lift.thy \ |
31 CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy \ |
32 One.thy Pcpo.thy Pcpodef.thy Porder.thy ROOT.ML Sprod.thy Ssum.thy \ |
32 Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy \ |
33 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
33 LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy SetPcpo.thy \ |
34 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
34 Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML \ |
35 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
35 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
36 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |
36 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
37 Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex \ |
37 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
38 holcf_logic.ML |
38 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |
|
39 Tools/pcpodef_package.ML document/root.tex holcf_logic.ML |
39 @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
40 @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
40 |
41 |
41 |
42 |
42 ## HOLCF-IMP |
43 ## HOLCF-IMP |
43 |
44 |