equal
deleted
inserted
replaced
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 Bifinite.thy Cfun.thy \ |
31 CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy \ |
31 CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy \ |
32 Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy \ |
32 Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy \ |
33 LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy Cset.thy \ |
33 LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy \ |
34 Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML \ |
34 Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML \ |
35 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
35 Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML \ |
36 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
36 Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML \ |
37 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
37 Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML \ |
38 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |
38 Tools/domain/domain_theorems.ML Tools/fixrec_package.ML \ |