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 Bifinite.thy Cfun.thy \ |
30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Algebraic.thy Bifinite.thy Cfun.thy \ |
31 CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy \ |
31 CompactBasis.thy Completion.thy Cont.thy ConvexPD.thy Cprod.thy \ |
32 Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy \ |
32 Discrete.thy Deflation.thy Domain.thy Eventual.thy Ffun.thy \ |
33 LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy \ |
33 Fixrec.thy Fix.thy HOLCF.thy Lift.thy LowerPD.thy NatIso.thy \ |
34 Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML \ |
34 One.thy Pcpodef.thy Pcpo.thy Porder.thy Sprod.thy Ssum.thy Tr.thy \ |
|
35 Universal.thy UpperPD.thy Up.thy ROOT.ML \ |
35 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
36 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
36 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
37 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
37 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
38 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
38 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |
39 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |
39 Tools/pcpodef_package.ML document/root.tex holcf_logic.ML |
40 Tools/pcpodef_package.ML document/root.tex holcf_logic.ML |